change HasCompactSupport (rexp • (Ψ ∘ rexp))
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport fun x => rexp x • (Ψ ∘ rexp) x
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport (rexp • Ψ ∘ rexp)