Theorem: wiener_ikehara_smooth_sub (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
obtain ⟨ε, hε, hh⟩ := Metric.eventually_nhds_iff.mp <| comp_exp_support0 hplus
State after:
case intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)

State before:
case intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
apply tendsto_nhds_of_eventually_eq
State after:
case intro.intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
⊢ ∀ᶠ (x' : ℝ) in atTop, (↑A * ∫ (y : ℝ) in Ioi x'⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0

State before:
case intro.intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
⊢ ∀ᶠ (x' : ℝ) in atTop, (↑A * ∫ (y : ℝ) in Ioi x'⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
filter_upwards [eventually_gt_atTop ε⁻¹] with x hxε
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
have l1 : Integrable (indicator (Ioi x⁻¹) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
have l2 : Integrable (indicator (Ioi 0) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
simp_rw [← MeasureTheory.integral_indicator measurableSet_Ioi, ← mul_sub, ← integral_sub l1 l2]
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ↑A * ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ↑A * ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0
Tactic:
simp
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ A = 0 ∨ ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ A = 0 ∨ ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0
Tactic:
right
State after:
case h.h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0

State before:
case h.h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ∫ (a : ℝ), (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a = 0
Tactic:
apply MeasureTheory.integral_eq_zero_of_ae
State after:
case h.h.hf
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) =ᶠ[ae volume] 0

State before:
case h.h.hf
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) =ᶠ[ae volume] 0
Tactic:
apply eventually_of_forall
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ∀ (x_1 : ℝ), (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) x_1 = 0 x_1

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
⊢ ∀ (x_1 : ℝ), (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) x_1 = 0 x_1
Tactic:
intro t
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) t = 0 t

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ (fun a => (Ioi x⁻¹).indicator (fun y => Ψ y) a - (Ioi 0).indicator (fun y => Ψ y) a) t = 0 t
Tactic:
simp
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have hε' : 0 < ε⁻¹ := by positivity
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have hx : 0 < x := by linarith
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have hx' : 0 < x⁻¹ := by positivity
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have hεx : x⁻¹ < ε := by apply (inv_lt hε hx).mp hxε
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹) := by simp
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
have l5 := Set.indicator_union_of_disjoint l4 Ψ
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
Tactic:
rw [l3, l5]
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a) t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a) t = 0
Tactic:
ring_nf
State after:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ -(Ioc 0 x⁻¹).indicator Ψ t = 0

State before:
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ -(Ioc 0 x⁻¹).indicator Ψ t = 0
Tactic:
by_cases ht : t ∈ Ioc 0 x⁻¹ <;> simp [ht]
State after:
case pos
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : t ∈ Ioc 0 x⁻¹
⊢ Ψ t = 0

State before:
case pos
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : t ∈ Ioc 0 x⁻¹
⊢ Ψ t = 0
Tactic:
apply hh
State after:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : t ∈ Ioc 0 x⁻¹
⊢ dist t 0 < ε

State before:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : t ∈ Ioc 0 x⁻¹
⊢ dist t 0 < ε
Tactic:
simp at ht ⊢
State after:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ |t| < ε

State before:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ |t| < ε
Tactic:
have : |t| ≤ x⁻¹ := by rw [abs_le] ; constructor <;> linarith
State after:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
this : |t| ≤ x⁻¹
⊢ |t| < ε

State before:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
this : |t| ≤ x⁻¹
⊢ |t| < ε
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ 0 < ε⁻¹
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
⊢ 0 < x⁻¹
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
⊢ x⁻¹ < ε
Tactic:
apply (inv_lt hε hx).mp hxε
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
⊢ Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
Tactic:
ext t
State after:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ t ∈ Ioi 0 ↔ t ∈ Ioc 0 x⁻¹ ∪ Ioi x⁻¹

State before:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ t ∈ Ioi 0 ↔ t ∈ Ioc 0 x⁻¹ ∪ Ioi x⁻¹
Tactic:
simp
State after:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ 0 < t ↔ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t

State before:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ 0 < t ↔ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
Tactic:
constructor <;> intro h
State after:
case h.mp
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t
⊢ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t

case h.mpr
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
⊢ 0 < t

State before:
case h.mp
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t
⊢ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
Tactic:
simp [h, le_or_lt]
State after:
no goals

State before:
case h.mpr
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
⊢ 0 < t
Tactic:
cases h <;> linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
⊢ Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
Tactic:
simp
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ |t| ≤ x⁻¹
Tactic:
rw [abs_le]
State after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ -x⁻¹ ≤ t ∧ t ≤ x⁻¹

State before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ -x⁻¹ ≤ t ∧ t ≤ x⁻¹
Tactic:
constructor <;> linarith
State after:
no goals