internlm/Lean-Github huggingface dataset:
Theorem: second_fourier_integrable_aux1
Proof 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
Proof 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 <
    ⊤
Theorem: second_fourier_integrable_aux1
Proof 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
Proof 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 <
    ⊤
Theorem: second_fourier_integrable_aux1
Proof 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)
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 < σ'
ν : 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]
Proof state after:
no goals
Theorem: second_fourier_integrable_aux2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun u => cexp ((1 - ↑σ' - ↑t * I) * ↑u)) (Ioi (-x.log)) volume
Tactic:
refine (integrable_norm_iff (Measurable.aestronglyMeasurable <| by fun_prop)).mp ?_
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ Integrable (fun a => ‖cexp ((1 - ↑σ' - ↑t * I) * ↑a)‖) (volume.restrict (Ioi (-x.log)))
Theorem: second_fourier_integrable_aux2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ Integrable (fun a => ‖cexp ((1 - ↑σ' - ↑t * I) * ↑a)‖) (volume.restrict (Ioi (-x.log)))
Tactic:
suffices IntegrableOn (fun a ↦ rexp (-(σ' - 1) * a)) (Ioi (-x.log)) _ by simpa [Complex.abs_exp]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun a => rexp (-(σ' - 1) * a)) (Ioi (-x.log)) volume
Theorem: second_fourier_integrable_aux2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun a => rexp (-(σ' - 1) * a)) (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_aux2
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_aux2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ Measurable fun u => cexp ((1 - ↑σ' - ↑t * I) * ↑u)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: second_fourier_integrable_aux2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
this : IntegrableOn (fun a => rexp (-(σ' - 1) * a)) (Ioi (-x.log)) ?m.446246
⊢ Integrable (fun a => ‖cexp ((1 - ↑σ' - ↑t * I) * ↑a)‖) (volume.restrict (Ioi (-x.log)))
Tactic:
simpa [Complex.abs_exp]
Proof state after:
no goals
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ -(cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / (1 - ↑σ' - ↑t * I)) = ↑(x ^ (σ' - 1)) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
calc
  _ = cexp (↑(Real.log x) * ((↑σ' - 1) + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by rw [← div_neg]; ring_nf
  _ = (x ^ ((↑σ' - 1) + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by
    rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), Complex.ofReal_log hx.le]
  _ = (x ^ ((σ' : ℂ) - 1)) * (x ^ (↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by
    rw [Complex.cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt hx))]
  _ = _ := by rw [ofReal_cpow hx.le]; push_cast; ring
Proof state after:
no goals
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ -(cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / (1 - ↑σ' - ↑t * I)) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [← div_neg]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / -(1 - ↑σ' - ↑t * I) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / -(1 - ↑σ' - ↑t * I) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
ring_nf
Proof state after:
no goals
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1 + ↑t * I) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), Complex.ofReal_log hx.le]
Proof state after:
no goals
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1 + ↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [Complex.cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt hx))]
Proof state after:
no goals
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑(x ^ (σ' - 1)) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
rw [ofReal_cpow hx.le]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ ↑(σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ ↑(σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
push_cast
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Theorem: second_fourier_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
ring
Proof state after:
no goals
Theorem: second_fourier
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ (u / (2 * π)) =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
conv in ↑(rexp _) * _ => { rw [Real.fourierIntegral_real_eq, ← smul_eq_mul, ← integral_smul] }
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ∫ (a : ℝ), ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Theorem: second_fourier
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ∫ (a : ℝ), ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
rw [MeasureTheory.integral_integral_swap]
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)
Theorem: second_fourier
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

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

n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Theorem: second_fourier
Proof state before:
case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)

n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
exact second_fourier_integrable_aux1 hcont hsupp hσ
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Theorem: second_fourier
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
rw [← integral_mul_left]
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ∫ (a : ℝ), ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))
Theorem: second_fourier
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
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ∫ (a : ℝ), ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * 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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ (fun y => ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y) = fun a =>
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))
Theorem: second_fourier
Proof state before:
case e_f
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ (fun y => ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y) = fun a =>
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))
Tactic:
ext t
Proof state after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(t * (x / (2 * π)))) • ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Theorem: second_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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(t * (x / (2 * π)))) • ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
dsimp [Real.fourierChar, expMapCircle]
Proof state after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) * (cexp (↑(2 * π * -(t * (x / (2 * π)))) * I) * ψ t) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Theorem: second_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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) * (cexp (↑(2 * π * -(t * (x / (2 * π)))) * I) * ψ t) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
simp_rw [← mul_assoc _ _ (ψ _), integral_mul_right]
Proof state after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Theorem: second_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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
rw [fun (a b d : ℂ) ↦ show a * (b * (ψ t) * d) = (a * b * d) * ψ t by ring]
Proof state after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I) * ψ t
Theorem: second_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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I) * ψ t
Tactic:
congr 1
Proof state after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Theorem: second_fourier
Proof state before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
push_cast
Proof state after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1)) * cexp (2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Theorem: second_fourier
Proof state before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1)) * cexp (2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simp_rw [← Complex.exp_add]
Proof state after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)