awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| →
          ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2)‖ ≤
            rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |(-y)| ≤ |c|
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2)‖ ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))

Tactic:
simpa only [neg_mul, ofReal_neg] using vert_norm_bound hT absy

Premises used: Complex.ofReal_neg, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)
⊢ Tendsto (verticalIntegral b c) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ?_
      (Eventually.of_forall fun _ => norm_nonneg _)
      ((eventually_ge_atTop (0 : ℝ)).mp
        (Eventually.of_forall fun T hT => verticalIntegral_norm_le hb c hT))

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, GaussianFourier.verticalIntegral, Filter.Eventually.mp, Filter.eventually_ge_atTop, GaussianFourier.verticalIntegral_norm_le, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
tendsto_of_tendsto_of_tendsto_of_le_of_le' :
  Tendsto (β := ℝ)
    (fun (T : ℝ) ↦
      2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)

Tactic:
refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ?_
      (Eventually.of_forall fun _ => norm_nonneg _)
      ((eventually_ge_atTop (0 : ℝ)).mp
        (Eventually.of_forall fun T hT => verticalIntegral_norm_le hb c hT))

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.eventually_ge_atTop, GaussianFourier.verticalIntegral_norm_le, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ 0 = 2 * |c| * 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
rw :
  Tendsto
    (fun (T : ℝ) ↦
      2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
    atTop (𝓝 (2 * |c| * 0))
⊢ Tendsto (β := ℝ)
    (fun (T : ℝ) ↦
      2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
    atTop (𝓝 0)

Tactic:
rw [(by ring : 0 = 2 * |c| * 0)]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto
    (fun (T : ℝ) ↦
      2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
    atTop (𝓝 (2 * |c| * 0))

Tactic:
(tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _

Premises used: Filter.tendsto_neg_atTop_atBot, Real.exp, Filter.Tendsto.const_mul, Real.tendsto_exp_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
refine :
  Tendsto (β := ℝ) (fun (T : ℝ) ↦ b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)
    atTop atTop
⊢ Tendsto
    (fun (T : ℝ) ↦
      2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
    atTop (𝓝 (2 * |c| * 0))

Tactic:
refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.const_mul, Real.tendsto_exp_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b.re * HPow.hPow (β := ℕ) x 2 - 2 * |b.im| * |c| * x) atTop atTop
⊢ Tendsto (β := ℝ) (fun (T : ℝ) ↦ b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)
    atTop atTop

Tactic:
apply tendsto_atTop_add_const_right

Premises used: Filter.tendsto_atTop_add_const_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b.re * HPow.hPow (β := ℕ) x 2 - 2 * |b.im| * |c| * x) atTop atTop

Tactic:
simp_rw [sq, ← mul_assoc, ← sub_mul]

Premises used: mul_assoc, sq, sub_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop

Tactic:
Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id

Premises used: Filter.tendsto_atTop_add_const_right, Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
hf : Tendsto (α := ℝ) (HMul.hMul b.re) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop

Tactic:
refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id

Premises used: Filter.tendsto_atTop_add_const_right, Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (α := ℝ) (HMul.hMul b.re) atTop atTop

Tactic:
(tendsto_const_mul_atTop_of_pos hb).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (α := ℝ) (HMul.hMul b.re) atTop atTop

Tactic:
exact (tendsto_const_mul_atTop_of_pos hb).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
refine :
  @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
rw :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑a : ℂ) + (↑c : ℂ) * I) 2)‖) volume
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) volume

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
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
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑a : ℂ) + (↑c : ℂ) * I) 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]

Premises used: neg_sub, HMul.hMul, sub_eq_add_neg, Complex.re, LT.lt.ne', GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I', HPow.hPow, OfNat.ofNat, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume
⊢ @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:
(Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _

Premises used: HMul.hMul, Complex.im, HDiv.hDiv, Complex.re, MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.Integrable.hasFiniteIntegral, MeasureTheory.Integrable.comp_sub_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume
⊢ @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:
exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _

Premises used: HMul.hMul, Complex.im, HDiv.hDiv, Complex.re, MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.Integrable.hasFiniteIntegral, MeasureTheory.Integrable.comp_sub_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
suffices :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume
⊢ @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:
suffices Integrable fun x : ℝ => exp (-(b.re * x ^ 2)) by
    exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
simp_rw :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-(b.re * HPow.hPow (β := ℕ) x 2))) volume

Tactic:
simp_rw [← neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) volume

Tactic:
apply integrable_exp_neg_mul_sq hb

Premises used: integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)

Tactic:
tendsto_nhds_unique
      (intervalIntegral_tendsto_integral (integrable_cexp_neg_mul_sq_add_real_mul_I hb c)
        tendsto_neg_atTop_atBot tendsto_id)
      ?_

Premises used: GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I, Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, MeasureTheory.intervalIntegral_tendsto_integral, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
hb₁ :
  Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
    (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) =
    ((↑π : ℂ) / 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)
      ?_

Premises used: GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I, Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, MeasureTheory.intervalIntegral_tendsto_integral, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ 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₁

Premises used: HMul.hMul, intervalIntegral, Complex.ofReal, HPow.hPow, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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)

Tactic:
Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp

Premises used: Differentiable.cexp, Differentiable.const_mul, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : ℝ
refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-b * HPow.hPow (β := ℕ) z 2))
    (uIcc (-(↑T : ℂ)).re ((↑T : ℂ) + (↑c : ℂ) * I).re ×ℂ uIcc (-(↑T : ℂ)).im ((↑T : ℂ) + (↑c : ℂ) * I).im)

Tactic:
refine Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp

Premises used: Differentiable.cexp, Differentiable.const_mul, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : ℝ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2

Tactic:
differentiable_pow 2

Premises used: differentiable_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : ℝ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2

Tactic:
exact differentiable_pow 2

Premises used: differentiable_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : ℝ
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : ℝ
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
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0

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

Premises used: Complex.mul_im, Complex.add_im, Complex.mul_re, MulZeroClass.zero_mul, Complex.ofReal_neg, Complex.add_re, Complex.I_re, zero_add, Complex.I_im, MulZeroClass.mul_zero, tsub_zero, Complex.ofReal_zero, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im, smul_eq_mul, mul_one, add_zero, neg_zero, Complex.neg_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
simp_rw : Tendsto I₁ atTop (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * HPow.hPow (β := ℕ) ((↑x : ℂ) + (↑c : ℂ) * I) 2)) atTop
    (𝓝 (((↑π : ℂ) / b) ^ (1 / 2)))

Tactic:
simp_rw [id, ← HI₁]

Premises used: id
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
h : ∀ (T : ℝ), I₁ T = I₂ T + verticalIntegral b c T
⊢ I₁ = fun (T : ℝ) ↦ I₂ T + verticalIntegral b c T

Tactic:
ext1 T