internlm/Lean-Github huggingface dataset:
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 (-(σ' - 1) * x)) (Ioi (-x.log)) volume
Tactic:
apply exp_neg_integrableOn_Ioi
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ 0 < σ' - 1
Theorem: second_fourier_integrable_aux1a
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ 0 < σ' - 1
Tactic:
linarith
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 < σ'
a x : ℝ
⊢ -(x * a) = -a * x
Tactic:
ring
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
⊢ let ν := (volume.restrict (Ici (-x.log))).prod volume;
  Integrable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
intro ν
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ Integrable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Theorem: second_fourier_integrable_aux1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ Integrable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
constructor
Proof state after:
case left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ AEStronglyMeasurable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Theorem: second_fourier_integrable_aux1
Proof state before:
case left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ AEStronglyMeasurable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
apply Measurable.aestronglyMeasurable
Proof state after:
case left.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ Measurable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a)
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ Measurable
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a)
Tactic:
apply MeasureTheory.measurable_uncurry_of_continuous_of_measurable <;> intro i
Proof state after:
case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i

case left.hf.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Measurable fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i

case left.hf.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Measurable fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a
Tactic:
swap
Proof state after:
case left.hf.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Measurable fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a

case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Measurable fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a

case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i
Tactic:
apply Continuous.measurable
Proof state after:
case left.hf.h.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a

case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun a => ↑(rexp (-i * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (i / (2 * π)))))) • ψ a
Tactic:
apply Continuous.smul
Proof state after:
case left.hf.h.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(rexp (-i * (σ' - 1)))

case left.hf.h.hf.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π)))))) • ψ x
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(rexp (-i * (σ' - 1)))
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π)))))) • ψ x
Tactic:
apply Continuous.smul
Proof state after:
case left.hf.h.hf.hg.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π))))))

case left.hf.h.hf.hg.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ψ x
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hg.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π))))))
Tactic:
apply Continuous.subtype_val
Proof state after:
case left.hf.h.hf.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => 𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π)))))
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => 𝐞 (Multiplicative.ofAdd (-(x * (i / (2 * π)))))
Tactic:
simp [Real.fourierChar, expMapCircle, Multiplicative.ofAdd]
Proof state after:
case left.hf.h.hf.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ⟨cexp (-(2 * ↑π * (↑x * (↑i / (2 * ↑π))) * I)), ⋯⟩
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ⟨cexp (-(2 * ↑π * (↑x * (↑i / (2 * ↑π))) * I)), ⋯⟩
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.h.hf.hg.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ψ x
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun i_1 => ↑(rexp (-i_1 * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(i * (i_1 / (2 * π)))))) • ψ i
Tactic:
apply Continuous.smul
Proof state after:
case left.hf.hu_cont.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(rexp (-x * (σ' - 1)))

case left.hf.hu_cont.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π)))))) • ψ i
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(rexp (-x * (σ' - 1)))
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π)))))) • ψ i
Tactic:
apply Continuous.smul
Proof state after:
case left.hf.hu_cont.hg.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π))))))

case left.hf.hu_cont.hg.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ψ i
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hg.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ↑(𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π))))))
Tactic:
apply Continuous.subtype_val
Proof state after:
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => 𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π)))))
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => 𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π)))))
Tactic:
simp [Real.fourierChar, expMapCircle, Multiplicative.ofAdd]
Proof state after:
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ⟨cexp (-(2 * ↑π * (↑i * (↑x / (2 * ↑π))) * I)), ⋯⟩
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ⟨cexp (-(2 * ↑π * (↑i * (↑x / (2 * ↑π))) * I)), ⋯⟩
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case left.hf.hu_cont.hg.hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ψ i
Tactic:
continuity
Proof state after:
no goals
Theorem: second_fourier_integrable_aux1
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
let f1 : ℝ → ENNReal := fun a1 ↦ ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Theorem: second_fourier_integrable_aux1
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
let f2 : ℝ → ENNReal := fun a2 ↦ ↑‖ψ a2‖₊
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Theorem: second_fourier_integrable_aux1
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
suffices ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤ by simpa [Function.uncurry, HasFiniteIntegral]
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤
Theorem: second_fourier_integrable_aux1
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤
Tactic:
refine (lintegral_prod_mul ?_ ?_).trans_lt ?_ <;> unfold_let f1 f2
Proof state after:
case right.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ AEMeasurable (fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊) (volume.restrict (Ici (-x.log)))

case right.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ AEMeasurable (fun a2 => ↑‖ψ a2‖₊) volume

case right.refine_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
⊢ (∫⁻ (x : ℝ) in Ici (-x.log), (fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊) x) *
      ∫⁻ (y : ℝ), (fun a2 => ↑‖ψ a2‖₊) y ∂volume <
    ⊤