awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume
have refine : @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
  (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume
have rw : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
  (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑a : ℂ) + (↑c : ℂ) * I) 2)‖) volume
Tactic: rw [← hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑a : ℂ) + (↑c : ℂ) * I) 2)‖) volume
have simp_rw : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
  (fun (a : ℝ) ↦
    rexp (HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)) *
      rexp (-(b.re * HPow.hPow (β := ℕ) (a - b.im * c / b.re) 2)))
  volume
Tactic: simp_rw [norm_cexp_neg_mul_sq_add_mul_I' hb.ne', neg_sub _ (c ^ 2 * _),
    sub_eq_add_neg _ (b.re * _), Real.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦
      rexp (HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)) *
        rexp (-(b.re * HPow.hPow (β := ℕ) (a - b.im * c / b.re) 2)))
    volume
have suffices : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume
Tactic: suffices Integrable fun x : ℝ => exp (-(b.re * x ^ 2)) by
    exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume
have simp_rw : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) volume
Tactic: simp_rw [← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have hb₁ : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
  (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
Tactic: refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral (integrable_cexp_neg_mul_sq_add_real_mul_I hb c)
        tendsto_neg_atTop_atBot tendsto_id)
      ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
    (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
have HI₁ : let I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2);
I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
Tactic: set I₁ := fun T => ∫ x : ℝ in -T..T, cexp (-b * (x + c * I) ^ 2) with HI₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2))
    (uIcc (-(↑T : ℂ)).re ((↑T : ℂ) + (↑c : ℂ) * I).re ×ℂ uIcc (-(↑T : ℂ)).im ((↑T : ℂ) + (↑c : ℂ) * I).im)
have refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2
Tactic: refine Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
have this : HSub.hSub (α := ℂ)
        (∫ (x : ℝ) in (-(↑T : ℂ)).re..((↑T : ℂ) + (↑c : ℂ) * I).re,
          (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2)) ((↑x : ℂ) + (↑(-(↑T : ℂ)).im : ℂ) * I))
        (∫ (x : ℝ) in (-(↑T : ℂ)).re..((↑T : ℂ) + (↑c : ℂ) * I).re,
          (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2)) ((↑x : ℂ) + (↑((↑T : ℂ) + (↑c : ℂ) * I).im : ℂ) * I)) +
      HSMul.hSMul (β := ℂ) I
        (∫ (y : ℝ) in (-(↑T : ℂ)).im..((↑T : ℂ) + (↑c : ℂ) * I).im,
          (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2)) ((↑((↑T : ℂ) + (↑c : ℂ) * I).re : ℂ) + (↑y : ℂ) * I)) -
    HSMul.hSMul (β := ℂ) I
      (∫ (y : ℝ) in (-(↑T : ℂ)).im..((↑T : ℂ) + (↑c : ℂ) * I).im,
        (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2)) ((↑(-(↑T : ℂ)).re : ℂ) + (↑y : ℂ) * I)) =
  0
Tactic: have :=
      integral_boundary_rect_eq_zero_of_differentiableOn (fun z => cexp (-b * z ^ 2)) (-T)
        (T + c * I)
        (by
          refine Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp
          exact differentiable_pow 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
    (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
have C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
Tactic: have C : ∀ T : ℝ, I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0 := by
    intro T
    have :=
      integral_boundary_rect_eq_zero_of_differentiableOn (fun z => cexp (-b * z ^ 2)) (-T)
        (T + c * I)
        (by
          refine Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp
          exact differentiable_pow 2)
    simpa only [neg_im, ofReal_im, neg_zero, ofReal_zero, zero_mul, add_zero, neg_re,
      ofReal_re, add_re, mul_re, I_re, mul_zero, I_im, tsub_zero, add_im, mul_im,
      mul_one, zero_add, smul_eq_mul, ofReal_neg] using this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
    (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
have simp_rw : Tendsto I₁ atTop (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
Tactic: simp_rw [id, ← HI₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T
have h : ∀ (T : ℝ), I₁ T = I₂ T + verticalIntegral b c T
Tactic: ext1 T
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
T : ℝ
⊢ I₁ T = I₂ T + verticalIntegral b c T
have C₁ : I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
Tactic: specialize C T
Cleared hypotheses: C
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ I₁ T = I₂ T + verticalIntegral b c T
have C₁ : I₂ T - I₁ T + I * I₄ T = I * I₅ T
Tactic: rw [sub_eq_zero] at C
Cleared hypotheses: C
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T +
      ∫ (y : ℝ) in 0..c,
        I *
          (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
            cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))
have h : I₁ T =
  I₂ T +
    I *
      HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
        (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))
Tactic: rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h :
  I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))
⊢ I₁ T =
    I₂ T +
      ∫ (y : ℝ) in 0..c,
        I *
          (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
            cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))
have h₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)) volume 0 c
Tactic: rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
h :
  I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))
h₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)) volume 0 c
⊢ I₁ T =
    I₂ T +
      ∫ (y : ℝ) in 0..c,
        I *
          (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
            cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))
have h₂ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)) volume 0 c
Tactic: rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b_1 : ℂ
hb : 0 < b_1.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b_1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b_1 * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
a b : ℂ
⊢ HPow.hPow (β := ℕ) (a - b * I) 2 = HPow.hPow (β := ℕ) (-a + b * I) 2
have rw : (a - b * I) * (a - b * I) = HPow.hPow (β := ℕ) (-a + b * I) 2
Tactic: rw [sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T +
      I *
        HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
          (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))
have h : I₁ T =
  I₂ T +
    I *
      HSub.hSub (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2))
        (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑x : ℂ) * I) 2))
Tactic: simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + I * (I₄ T - I₅ T)
have h : I₁ T = I₂ T + (I * I₄ T - (I₂ T - I₁ T + I * I₄ T))
Tactic: rw [mul_sub, ← C]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)) volume 0 c
have h : Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2)
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)) volume 0 c
have h : Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2)
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ Tendsto I₁ atTop (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
have this : I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T
Tactic: have : I₁ = fun T : ℝ => I₂ T + verticalIntegral b c T := by
    ext1 T
    specialize C T
    rw [sub_eq_zero] at C
    unfold verticalIntegral
    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
    · simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
      change I₁ T = I₂ T + I * (I₄ T - I₅ T)
      rw [mul_sub, ← C]
      abel
    all_goals apply Continuous.intervalIntegrable; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
this : I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T
⊢ Tendsto I₁ atTop (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
have rw : Tendsto (fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T) atTop
  (𝓝
    (HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      0))
Tactic: rw [this, ← add_zero ((π / b : ℂ) ^ (1 / 2 : ℂ)), ← integral_gaussian_complex hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
HI₁ : I₁ = fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)
I₂ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (x : ℝ) in -T..T, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
I₄ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)
I₅ : (T : ℝ) → ℂ := fun (T : ℝ) ↦ ∫ (y : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (-(↑T : ℂ) + (↑y : ℂ) * I) 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
this : I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T
⊢ Tendsto (fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T) atTop
    (𝓝
      (HAdd.hAdd (α := ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
          cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        0))
have refine : Tendsto I₂ atTop
  (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
Tactic: refine Tendsto.add ?_ (tendsto_verticalIntegral hb c)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ b ≠ 0
have contrapose! : ∀ (hb : b = 0), 0 ≤ b.re
Tactic: contrapose! hb
Cleared hypotheses: hb