awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ)))
    (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
have rw : Eq (α := ℂ)
  (∏ i : ι,
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
  (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
Tactic: rw [integral_fintype_prod_volume_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Eq (α := ℂ)
    (∏ i : ι,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
have e_f : ∀ (i : ι),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
    ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
    ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))
have this : (-b i).re < 0
Tactic: have : (-b i).re < 0 := by simpa using hb i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
    ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))
have h : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
    cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
    cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0))
Tactic: convert! integral_cexp_quadratic this (c i) 0 using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
h :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
    ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))
have h₁ : ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)) =
  ((↑π : ℂ) / - -b i) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (c i) 2 / (4 * -b i))
Tactic: convert! integral_cexp_quadratic this (c i) 0 using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
    cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
    cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₂ : ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₃ : ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₃ :
  ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₄ : HMul.hMul (α := ℂ) (∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹)
    (∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₃ :
  ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₄ :
  HMul.hMul (α := ℂ) (∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹)
      (∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₅ : HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ ^ Finset.card.{u_2} (α := ι) Finset.univ *
    ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₃ :
  ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₄ :
  HMul.hMul (α := ℂ) (∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹)
      (∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₅ :
  HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ ^ Finset.card.{u_2} (α := ι) Finset.univ *
      ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₆ : ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
    ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₃ :
  ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₄ :
  HMul.hMul (α := ℂ) (∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹)
      (∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₅ :
  HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ ^ Finset.card.{u_2} (α := ι) Finset.univ *
      ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₆ :
  ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
      ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₇ : ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
    cexp (∑ x : ι, HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 * cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : EuclideanSpace ℝ ι) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have rw : (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
    cexp
      (-b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2 +
        c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
    cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
Tactic: rw [← (PiLp.volume_preserving_toLp ι).integral_comp
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2 +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have simp : (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
    cexp
      (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
        c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
    cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
Tactic: simp only [neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h : ∀ (y : ι → ℝ),
  -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
    -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2
Tactic: convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h :
  ∀ (y : ι → ℝ),
    -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
      -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h₁ : ∀ (y : ι → ℝ), c * (↑⟪w, WithLp.toLp 2 y⟫ : ℂ) = ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(y i) : ℂ)
Tactic: convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h :
  ∀ (y : ι → ℝ),
    -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
      -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2
h₁ : ∀ (y : ι → ℝ), c * (↑⟪w, WithLp.toLp 2 y⟫ : ℂ) = ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(y i) : ℂ)
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h₂ : HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (c * (↑(w.ofLp i) : ℂ)) 2
Tactic: convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y