internlm/Lean-Github huggingface dataset:
Theorem: decay_bounds_W21
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∀ (t : ℝ), ‖(W1.deriv f).deriv.toFun t‖ ≤ A / (1 + t ^ 2)
Tactic:
exact hA'
Proof state after:
no goals
Theorem: decay_bounds
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hA : ∀ (t : ℝ), ‖ψ.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv^[2] ψ.toFun t‖ ≤ A / (1 + t ^ 2)
⊢ ‖𝓕 ψ.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
exact decay_bounds_W21 ψ hA hA' u
Proof state after:
no goals
Theorem: decay_bounds_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
have l1 : HasCompactSupport (fun u : ℝ => ((1 + u ^ 2) : ℝ) * ψ u) := by exact ψ.h2.mul_left
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
have := ψ.h1.continuous
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
obtain ⟨C, hC⟩ := l1.exists_bound_of_continuous (by continuity)
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
refine ⟨C, fun u => ?_⟩
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
u : ℝ
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
u : ℝ
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
specialize hC u
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : ‖↑(1 + u ^ 2) * ψ.toFun u‖ ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : ‖↑(1 + u ^ 2) * ψ.toFun u‖ ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
simp only [norm_mul, Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self.mpr (one_add_sq_pos u).le] at hC
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : (1 + u ^ 2) * Complex.abs (ψ.toFun u) ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Theorem: decay_bounds_cor_aux
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : (1 + u ^ 2) * Complex.abs (ψ.toFun u) ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
rwa [le_div_iff' (one_add_sq_pos _)]
Proof state after:
no goals
Theorem: decay_bounds_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
⊢ HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
Tactic:
exact ψ.h2.mul_left
Proof state after:
no goals
Theorem: decay_bounds_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ Continuous fun u => ↑(1 + u ^ 2) * ψ.toFun u
Tactic:
continuity
Proof state after:
no goals
Theorem: decay_bounds_cor
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
⊢ ∃ C, ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
simpa only [div_eq_mul_inv] using ⟨_, decay_bounds_key ψ⟩
Proof state after:
no goals
Theorem: continuous_FourierIntegral
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
⊢ Continuous fun p => ((innerₗ ℝ) p.1) p.2
Tactic:
exact continuous_mul
Proof state after:
no goals
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Tactic:
have l1 (C) : Integrable (fun u ↦ C / (1 + (u / c) ^ 2)) volume := by
  simpa using (integrable_inv_one_add_sq.comp_div hc).const_mul C
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Tactic:
have l2 : AEStronglyMeasurable (fun u ↦ 𝓕 ψ (u / c)) volume := by
  apply Continuous.aestronglyMeasurable ; continuity
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Tactic:
obtain ⟨C, h⟩ := decay_bounds_cor ψ
Proof state after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
C : ℝ
h : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Theorem: W21.integrable_fourier
Proof state before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
C : ℝ
h : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / c)) volume
Tactic:
apply @Integrable.mono' ℝ ℂ _ volume _ _ (fun u => C / (1 + (u / c) ^ 2)) (l1 C) l2 ?_
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
C : ℝ
h : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᵐ (a : ℝ), ‖𝓕 ψ.toFun (a / c)‖ ≤ (fun u => C / (1 + (u / c) ^ 2)) a
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
l2 : AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
C : ℝ
h : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᵐ (a : ℝ), ‖𝓕 ψ.toFun (a / c)‖ ≤ (fun u => C / (1 + (u / c) ^ 2)) a
Tactic:
apply eventually_of_forall (fun x => h _)
Proof state after:
no goals
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
C : ℝ
⊢ Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
Tactic:
simpa using (integrable_inv_one_add_sq.comp_div hc).const_mul C
Proof state after:
no goals
Theorem: W21.integrable_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
⊢ AEStronglyMeasurable (fun u => 𝓕 ψ.toFun (u / c)) volume
Tactic:
apply Continuous.aestronglyMeasurable
Proof state after:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
⊢ Continuous fun u => 𝓕 ψ.toFun (u / c)
Theorem: W21.integrable_fourier
Proof state before:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hc : c ≠ 0
l1 : ∀ (C : ℝ), Integrable (fun u => C / (1 + (u / c) ^ 2)) volume
⊢ Continuous fun u => 𝓕 ψ.toFun (u / c)
Tactic:
continuity
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
l2 : ∀ (n : ℕ) (x : ℝ), ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
⊢ Continuous fun x => LSeries f (↑σ' + ↑x * I)
Tactic:
exact continuous_tsum l1 hf (fun n x => le_of_eq (l2 n x))
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
by_cases h : i = 0
Proof state after:
case pos
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i

case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Theorem: continuous_LSeries_aux
Proof state before:
case pos
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
simpa [h] using continuous_const
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
simpa [h] using continuous_const.div (continuous_const.cpow (by continuity) (by simp [h])) (fun x => by simp [h])
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => ↑σ' + ↑x * I
Tactic:
continuity
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ ℝ → ↑i ∈ slitPlane
Tactic:
simp [h]
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
x : ℝ
⊢ ↑i ^ (↑σ' + ↑x * I) ≠ 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
by_cases h : n = 0
Proof state after:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n

case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Theorem: continuous_LSeries_aux
Proof state before:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
simp [h, nterm]
Proof state after:
no goals
Theorem: continuous_LSeries_aux
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
field_simp [h, nterm, cpow_add _ _ (Nat.cast_ne_zero.mpr h)]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ Complex.abs (↑n ^ (↑x * I)) = 1 ∨ f n = 0
Theorem: continuous_LSeries_aux
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ Complex.abs (↑n ^ (↑x * I)) = 1 ∨ f n = 0
Tactic:
rw [← Complex.norm_eq_abs, Complex.norm_natCast_cpow_of_pos (Nat.pos_of_ne_zero h)]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ↑n ^ (↑x * I).re = 1 ∨ f n = 0
Theorem: continuous_LSeries_aux
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ↑n ^ (↑x * I).re = 1 ∨ f n = 0
Tactic:
simp
Proof state after:
no goals
Theorem: limiting_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have hint : Integrable ψ := ψ.h1.continuous.integrable_of_hasCompactSupport ψ.h2
Proof state after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Theorem: limiting_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l3 : 0 < x := zero_lt_one.trans_le hx
Proof state after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Theorem: limiting_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l1 (σ') (hσ' : 1 < σ') := first_fourier hf ψ.h1.continuous hint l3 hσ'
Proof state after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Theorem: limiting_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l2 (σ') (hσ' : 1 < σ') := second_fourier ψ.h1.continuous hint l3 hσ'
Proof state after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Theorem: limiting_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l8 : Continuous fun t : ℝ ↦ (x : ℂ) ^ (t * I) :=
  continuous_const.cpow (continuous_ofReal.mul continuous_const) (by simp [l3])
Proof state after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)