internlm/Lean-Github huggingface dataset:
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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]
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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ε
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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 Ψ
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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]
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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]
Proof 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
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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 < ε
Theorem: wiener_ikehara_smooth_sub
Proof 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 ⊢
Proof 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| < ε
Theorem: wiener_ikehara_smooth_sub
Proof 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
Proof 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| < ε