internlm/Lean-Github huggingface dataset:
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]
Proof state after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ↑((↑n).log - x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ↑((↑n).log - x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
push_cast
Proof state after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - ↑x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - ↑x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
rw [Complex.ofReal_log hx.le]
Proof state after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - (↑x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - (↑x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
ring
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ 0 < ↑n
Tactic:
simpa using Nat.pos_iff_ne_zero.mpr hn
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ ↑x ≠ 0
Tactic:
simp [hx.ne.symm]
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ ↑n ≠ 0
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ (f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)) * ψ y = f n / ↑n ^ (↑σ' + ↑y * I) * (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)) * ψ y = f n / ↑n ^ (↑σ' + ↑y * I) * (ψ y * ↑x ^ (↑y * I))
Tactic:
group
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log) =
    ∑' (n : ℕ), term f (↑σ') n * ∫ (v : ℝ), 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
rfl
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * ∫ (v : ℝ), 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∑' (n : ℕ), ∫ (v : ℝ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
simp [integral_mul_left]
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), ∫ (v : ℝ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∫ (v : ℝ), ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
refine (integral_tsum ?_ ?_).symm
Proof state after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∀ (i : ℕ), AEStronglyMeasurable (fun v => term f (↑σ') i * 𝐞 (-(v * (1 / (2 * π) * (↑i / x).log))) • ψ v) volume

case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i * 𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Theorem: first_fourier
Proof state before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∀ (i : ℕ), AEStronglyMeasurable (fun v => term f (↑σ') i * 𝐞 (-(v * (1 / (2 * π) * (↑i / x).log))) • ψ v) volume
Tactic:
refine fun _ ↦ Measurable.aestronglyMeasurable ?_
Proof state after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝ * 𝐞 (-(v * (1 / (2 * π) * (↑x✝ / x).log))) • ψ v
Theorem: first_fourier
Proof state before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝ * 𝐞 (-(v * (1 / (2 * π) * (↑x✝ / x).log))) • ψ v
Tactic:
refine Measurable.mul (by fun_prop) ((Measurable.comp ?_ (by fun_prop)).smul (by fun_prop))
Proof state after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable ⇑𝐞
Theorem: first_fourier
Proof state before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable ⇑𝐞
Tactic:
exact Continuous.measurable Real.continuous_fourierChar
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝
Tactic:
fun_prop
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => -(v * (1 / (2 * π) * (↑x✝ / x).log))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => ψ v
Tactic:
fun_prop
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i * 𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Tactic:
simp_rw [nnnorm_mul]
Proof state after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑(‖term f (↑σ') i‖₊ * ‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊) ≠ ⊤
Theorem: first_fourier
Proof state before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑(‖term f (↑σ') i‖₊ * ‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊) ≠ ⊤
Tactic:
push_cast
Proof state after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i‖₊ * ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Theorem: first_fourier
Proof state before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i‖₊ * ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Tactic:
simp_rw [lintegral_const_mul _ (first_fourier_aux1 hcont _)]
Proof state after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume ≠ ⊤
Theorem: first_fourier
Proof state before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume ≠ ⊤
Tactic:
calc
  _ = (∑' (i : ℕ), (‖term f σ' i‖₊ : ENNReal)) * ∫⁻ (a : ℝ), ‖ψ a‖₊ ∂volume := by
    simp [ENNReal.tsum_mul_right]
  _ ≠ ⊤ := ENNReal.mul_ne_top (hf_coe1 hf hσ)
    (ne_top_of_lt hsupp.2)
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume =
    (∑' (i : ℕ), ↑‖term f (↑σ') i‖₊) * ∫⁻ (a : ℝ), ↑‖ψ a‖₊
Tactic:
simp [ENNReal.tsum_mul_right]
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (v : ℝ), ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)
Tactic:
congr 1
Proof state after:
case e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ (fun v => ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v) = fun t =>
    LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)
Theorem: first_fourier
Proof state before:
case e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ (fun v => ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v) = fun t =>
    LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)
Tactic:
ext y
Proof state after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    LSeries f (↑σ' + ↑y * I) * ψ y * ↑x ^ (↑y * I)
Theorem: first_fourier
Proof state before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    LSeries f (↑σ' + ↑y * I) * ψ y * ↑x ^ (↑y * I)
Tactic:
simp_rw [mul_assoc (LSeries _ _), ← smul_eq_mul (a := (LSeries _ _)), LSeries]
Proof state after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (∑' (n : ℕ), term f (↑σ' + ↑y * I) n) • (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier
Proof state before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (∑' (n : ℕ), term f (↑σ' + ↑y * I) n) • (ψ y * ↑x ^ (↑y * I))
Tactic:
rw [← tsum_smul_const]
Proof state after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    ∑' (z : ℕ), term f (↑σ' + ↑y * I) z • (ψ y * ↑x ^ (↑y * I))

case e_f.h.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun n => term f (↑σ' + ↑y * I) n
Theorem: first_fourier
Proof state before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    ∑' (z : ℕ), term f (↑σ' + ↑y * I) z • (ψ y * ↑x ^ (↑y * I))
Tactic:
congr with n
Proof state after:
case e_f.h.e_f.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier
Proof state before:
case e_f.h.e_f.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
exact first_fourier_aux2 hx n
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
case e_f.h.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun n => term f (↑σ' + ↑y * I) n
Tactic:
apply Summable.of_norm
Proof state after:
case e_f.h.hf.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun a => ‖term f (↑σ' + ↑y * I) a‖
Theorem: first_fourier
Proof state before:
case e_f.h.hf.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun a => ‖term f (↑σ' + ↑y * I) a‖
Tactic:
convert hf σ' hσ with n
Proof state after:
case h.e'_5.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Theorem: first_fourier
Proof state before:
case h.e'_5.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ ‖term f (↑σ' + ↑y * 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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : n = 0
⊢ ‖term f (↑σ' + ↑y * 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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Theorem: first_fourier
Proof state before:
case pos
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : n = 0
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Tactic:
simp [nterm, term, h]
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Tactic:
simp [nterm, term, h]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Theorem: first_fourier
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Tactic:
have : (n : ℂ) ≠ 0 := by simp [h]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
this : ↑n ≠ 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Theorem: first_fourier
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
this : ↑n ≠ 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Tactic:
simp [Complex.abs_cpow_of_ne_zero this]
Proof state after:
no goals
Theorem: first_fourier
Proof state before:
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => cexp (-(↑x * (↑σ' - 1)))) (Ici (-x.log)) volume
Tactic:
norm_cast
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => ↑(rexp (-(x * (σ' - 1))))) (Ici (-x.log)) volume
Theorem: second_fourier_integrable_aux1a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => ↑(rexp (-(x * (σ' - 1))))) (Ici (-x.log)) volume
Tactic:
suffices IntegrableOn (fun (x : ℝ) ↦ (rexp (-(x * (σ' - 1))))) (Ici (-x.log)) _ from this.ofReal
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => rexp (-(x * (σ' - 1)))) (Ici (-x.log)) volume
Theorem: second_fourier_integrable_aux1a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => rexp (-(x * (σ' - 1)))) (Ici (-x.log)) volume
Tactic:
simp_rw [fun (a x : ℝ) ↦ (by ring : -(x * a) = -a * x), integrableOn_Ici_iff_integrableOn_Ioi]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => rexp (-(σ' - 1) * x)) (Ioi (-x.log)) volume