awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
    b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
      HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)
rw :
  rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2)) =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
have rw₁ : rexp
    (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
        HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re))) =
  rexp
    (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
        HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
Tactic: rw [norm_cexp_neg_mul_sq_add_mul_I, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |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))
have rw : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * y * T - b.re * HPow.hPow (β := ℕ) y 2)) ≤
  rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: rw [norm_cexp_neg_mul_sq_add_mul_I b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * y * T - b.re * HPow.hPow (β := ℕ) y 2)) ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a : 2 * b.im * y ≤ 2 * |b.im| * |c|
Tactic: gcongr exp (-(_ - ?_ * _ - _ * ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
a : 2 * b.im * y ≤ 2 * |b.im| * |c|
⊢ rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * y * T - b.re * HPow.hPow (β := ℕ) y 2)) ≤
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a₁ : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) c 2
Tactic: gcongr exp (-(_ - ?_ * _ - _ * ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
| 2 * b.im * y
have rw : 2 * (b.im * y)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * b.im * y ≤ 2 * |b.im| * |c|
have a : 2 * (b.im * y) ≤ 2 * |b.im| * |c|
Tactic: conv_lhs => rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
| 2 * |b.im| * |c|
have rw : 2 * (|b.im| * |c|)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * (b.im * y) ≤ 2 * |b.im| * |c|
have a : 2 * (b.im * y) ≤ 2 * (|b.im| * |c|)
Tactic: conv_rhs => rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * (b.im * y) ≤ 2 * (|b.im| * |c|)
have a : b.im * y ≤ |b.im| * |c|
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ b.im * y ≤ |b.im| * |c|
have a : |b.im * y| ≤ |b.im| * |c|
Tactic: refine (le_abs_self _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ |b.im * y| ≤ |b.im| * |c|
have a : |b.im| * |y| ≤ |b.im| * |c|
Tactic: rw [abs_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c_1 T_1 : ℝ
hT_1 : 0 ≤ T_1
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ |b.im| * |y| ≤ |b.im| * |c|
have a : 0 ≤ |b.im|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
⊢ ‖verticalIntegral b c T‖ ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have 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))
Tactic: have vert_norm_bound :
    ∀ {T : ℝ},
      0 ≤ T →
        ∀ {c y : ℝ},
          |y| ≤ |c| →
            ‖cexp (-b * (T + y * I) ^ 2)‖ ≤
              exp (-(b.re * T ^ 2 - (2 : ℝ) * |b.im| * |c| * T - b.re * c ^ 2)) := by
    intro T hT c y hy
    rw [norm_cexp_neg_mul_sq_add_mul_I b]
    gcongr exp (-(_ - ?_ * _ - _ * ?_))
    · (conv_lhs => rw [mul_assoc]); (conv_rhs => rw [mul_assoc])
      gcongr _ * ?_
      refine (le_abs_self _).trans ?_
      rw [abs_mul]
      gcongr
    · rwa [sq_le_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ ‖verticalIntegral b c T‖ ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have apply : 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c - 0| ≤
  2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: apply (intervalIntegral.norm_integral_le_of_norm_le_const _).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
apply :
  2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c - 0| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
apply₁ : ℝ
⊢ ‖verticalIntegral b c T‖ ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have apply₂ : ∀ x ∈ uIoc 0 c,
  ‖I *
        (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑x : ℂ) * I) 2) -
          cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑x : ℂ) * I) 2))‖ ≤
    2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: apply (intervalIntegral.norm_integral_le_of_norm_le_const _).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c - 0| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have rw : 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c| ≤
  2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c|
have simp : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
Tactic: simp only [mul_comm _ |c|]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)) * |c| ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have conv_lhs : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
  2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: conv_lhs => simp only [mul_comm _ |c|]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a : 2 * |c|
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
a : 2 * |c|
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a₁ : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * |c|
have a : |c| * 2
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a : |c| * 2
Tactic: congr
        rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
a : |c| * 2
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have a₁ : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: congr
        rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have conv : |c| * 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: conv =>
        congr
        rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| |c| * 2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have rw : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
| 2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have conv : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
Tactic: conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
⊢ |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have conv_rhs : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
  2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: conv_rhs =>
      conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
conv_rhs :
  |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
⊢ |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
    2 * |c| * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have conv_rhs₁ : |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))) ≤
  |c| * (2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)))
Tactic: conv_rhs =>
      conv =>
        congr
        rw [mul_comm]
      rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
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
⊢ ‖I *
        (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
          cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))‖ ≤
    2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have absy : |y| ≤ |c|
Tactic: have absy : |y| ≤ |c| := by
      simpa using abs_sub_left_of_mem_uIcc (uIoc_subset_uIcc hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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|
⊢ ‖I *
        (cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
          cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) - (↑y : ℂ) * I) 2))‖ ≤
    2 * rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have rw : ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑y : ℂ) * I) 2) -
      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)) +
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
Tactic: rw [norm_mul, norm_I, one_mul, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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) -
        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)) +
      rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2))
have refine : ‖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: refine (norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
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))
have absy₁ : |(-y)| ≤ |c|
Tactic: rw [← abs_neg y] at absy
Cleared hypotheses: absy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (verticalIntegral b c) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖verticalIntegral b c x‖) atTop (𝓝 0)
have 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)
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))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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 (𝓝 0)
have 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))
Tactic: rw [(by ring : 0 = 2 * |c| * 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
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))
have refine : Tendsto (β := ℝ) (fun (T : ℝ) ↦ b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)
  atTop atTop
Tactic: refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (T : ℝ) ↦ b.re * HPow.hPow (β := ℕ) T 2 - 2 * |b.im| * |c| * T - b.re * HPow.hPow (β := ℕ) c 2)
    atTop atTop
have hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b.re * HPow.hPow (β := ℕ) x 2 - 2 * |b.im| * |c| * x) atTop atTop
Tactic: apply tendsto_atTop_add_const_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b.re * HPow.hPow (β := ℕ) x 2 - 2 * |b.im| * |c| * x) atTop atTop
have hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop
Tactic: simp_rw [sq, ← mul_assoc, ← sub_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop
have hf : Tendsto (α := ℝ) (HMul.hMul b.re) atTop atTop
Tactic: refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id