internlm/Lean-Github huggingface dataset:
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) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have (u : ℝ) :
    -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - σ' - t * I) * u := calc
  _ = -↑u * (↑σ' - 1) + (2 * ↑π) / (2 * ↑π) * -(↑t * ↑u) * I := by ring
  _ = -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I := by rw [div_self (by norm_num; exact pi_ne_zero)]
  _ = _ := by ring
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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simp_rw [this]
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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let c : ℂ := (1 - ↑σ' - ↑t * I)
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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have : c ≠ 0 := by simp [Complex.ext_iff, c] ; intro h ; linarith
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let f' (u : ℝ) := cexp (c * u)
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let f := fun (u : ℝ) ↦ (f' u) / c
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have hderiv : ∀ u ∈ Ici (-Real.log x), HasDerivAt f (f' u) u := by
  intro u _
  rw [show f' u = cexp (c * u) * (c * 1) / c by field_simp]
  exact (hasDerivAt_id' u).ofReal_comp.const_mul c |>.cexp.div_const c
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have hf : Tendsto f atTop (𝓝 0) := by
  apply tendsto_zero_iff_norm_tendsto_zero.mpr
  suffices Tendsto (fun (x : ℝ) ↦ abs (cexp (c * ↑x)) / abs c) atTop (𝓝 (0 / abs c)) by simpa [f, f'] using this
  apply Filter.Tendsto.div_const
  suffices Tendsto (. * (1 - σ')) atTop atBot by simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
  exact Tendsto.atTop_mul_neg_const (by linarith) fun ⦃s⦄ h ↦ h
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
rw [integral_Ici_eq_integral_Ioi,
  integral_Ioi_of_hasDerivAt_of_tendsto' hderiv (second_fourier_integrable_aux2 hσ) hf]
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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ 0 - f (-x.log) = ↑(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 : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ 0 - f (-x.log) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simpa [f, f'] using second_fourier_aux hx
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 < σ'
t : ℝ
a b d : ℂ
⊢ a * (b * ψ t * d) = a * b * d * ψ t
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 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = -↑u * (↑σ' - 1) + 2 * ↑π / (2 * ↑π) * -(↑t * ↑u) * 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 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 2 * ↑π / (2 * ↑π) * -(↑t * ↑u) * I = -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I
Tactic:
rw [div_self (by norm_num; exact pi_ne_zero)]
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 < σ'
t u : ℝ
⊢ 2 * ↑π ≠ 0
Tactic:
norm_num
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 < σ'
t u : ℝ
⊢ ¬π = 0
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 < σ'
t u : ℝ
⊢ ¬π = 0
Tactic:
exact pi_ne_zero
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 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I = (1 - ↑σ' - ↑t * I) * ↑u
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 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ c ≠ 0
Tactic:
simp [Complex.ext_iff, c]
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 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ 1 - σ' = 0 → ¬t = 0
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 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ 1 - σ' = 0 → ¬t = 0
Tactic:
intro 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 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
h : 1 - σ' = 0
⊢ ¬t = 0
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 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
h : 1 - σ' = 0
⊢ ¬t = 0
Tactic:
linarith
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
Tactic:
intro u _
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (f' u) u
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (f' u) u
Tactic:
rw [show f' u = cexp (c * u) * (c * 1) / c by field_simp]
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (cexp (c * ↑u) * (c * 1) / c) u
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (cexp (c * ↑u) * (c * 1) / c) u
Tactic:
exact (hasDerivAt_id' u).ofReal_comp.const_mul c |>.cexp.div_const c
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ f' u = cexp (c * ↑u) * (c * 1) / c
Tactic:
field_simp
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto f atTop (𝓝 0)
Tactic:
apply tendsto_zero_iff_norm_tendsto_zero.mpr
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)
Tactic:
suffices Tendsto (fun (x : ℝ) ↦ abs (cexp (c * ↑x)) / abs c) atTop (𝓝 (0 / abs c)) by simpa [f, f'] using this
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))
Tactic:
apply Filter.Tendsto.div_const
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)
Tactic:
suffices Tendsto (. * (1 - σ')) atTop atBot by simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => x * (1 - σ')) atTop atBot
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 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => x * (1 - σ')) atTop atBot
Tactic:
exact Tendsto.atTop_mul_neg_const (by linarith) fun ⦃s⦄ h ↦ h
Proof state after:
no goals