Theorem: second_fourier_integrable_aux1 (PrimeNumberTheoremAnd/Wiener.lean)

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 ν
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) ν

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
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) ν

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
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)

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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 * π)))))

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]
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)), ⋯⟩

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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 * π)))))

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]
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)), ⋯⟩

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
State after:
no goals

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
State after:
no goals

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)))‖₊
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) ν

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‖₊
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) ν

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]
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 ∂ν < ⊤

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
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 <
    ⊤

State before:
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 <
    ⊤
Tactic:
fun_prop
State after:
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 <
    ⊤

State before:
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 <
    ⊤
Tactic:
fun_prop
State after:
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 <
    ⊤

State before:
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 <
    ⊤
Tactic:
exact ENNReal.mul_lt_top (ne_top_of_lt (second_fourier_integrable_aux1a hσ).2)
  (ne_top_of_lt hsupp.2)
State after:
no goals

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
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
f2 : ℝ → ENNReal := fun a2 => ↑‖ψ a2‖₊
this : ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
Tactic:
simpa [Function.uncurry, HasFiniteIntegral]
State after:
no goals