awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
    atTop (𝓝 (f v))
have apply : EventuallyEq.{0, u_2} (β := E) atTop
  (fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
  fun (c : ℝ) ↦
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
Tactic: apply B.congr'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) c →
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
have h : ∀ (hc : 0 < c),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w)
Tactic: (hc : 0 < c)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
⊢ EventuallyEq.{0, u_2} (β := E) atTop
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w
have h : ∀ (c : ℝ) (hc : 0 < c),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w)
Tactic: filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
          cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
        f w)
have h : ∀ (w : V),
  ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
Tactic: congr with w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
have h : (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) • f w =
  (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
    f w
Tactic: rw [← coe_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) • f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
have h : (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) =
  ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
    cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
have h : (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) *
    cexp (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
  ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
    cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
Tactic: rw [ofReal_mul, ofReal_mul, ofReal_exp, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) *
      cexp (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
have h : (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) =
  ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) *
      cexp (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)
have h₁ : (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
  -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑((c ^ (1 / 2)) ^ finrank ℝ V) : ℂ) * (↑(π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
have h : (↑π : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) : ℂ) * (↑c : ℂ) ^ (↑(1 / 2 * (↑(finrank ℝ V) : ℝ)) : ℂ) =
  (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 * (↑c : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2
Tactic: rw [mul_cpow_ofReal_nonneg pi_nonneg hc.le, ← rpow_natCast, ← rpow_mul hc.le, mul_comm,
      ofReal_cpow pi_nonneg, ofReal_cpow hc.le]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
have h : -HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ HDiv.hDiv (α := ℝ) 1 2 • (v - w)‖ 2 =
  -HPow.hPow (β := ℕ) π 2 * c * HPow.hPow (β := ℕ) ‖v - w‖ 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ -HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ HDiv.hDiv (α := ℝ) 1 2 • (v - w)‖ 2 =
    -HPow.hPow (β := ℕ) π 2 * c * HPow.hPow (β := ℕ) ‖v - w‖ 2
have h : HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c ^ HMul.hMul (α := ℝ) 2⁻¹ (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ)) =
  HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ))
Tactic: simp only [one_div, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, neg_mul, neg_inj,
      ← rpow_natCast, ← rpow_mul hc.le, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
⊢ 𝓕⁻ (𝓕 f) = f
have h₁ : ∀ (v : V), 𝓕⁻ (𝓕 f) v = f v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕 (𝓕⁻ f) v = f v
have rw : 𝓕⁻ (𝓕 f) v = f v
Tactic: rw [fourierInv_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
⊢ 𝓕 (𝓕⁻ f) = f
have h₁ : ∀ (v : V), 𝓕 (𝓕⁻ f) v = f v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ 𝓕 (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕 f).toLp 2 volume
have h_dense : DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
  (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
Tactic: apply LinearMap.extendOfNorm_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h_dense :
  DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
⊢ 𝓕 (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕 f).toLp 2 volume
have h_norm : ∃ (C : ℝ),
  ∀ (x : 𝓢(E, F)),
    norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
            x :
          ↥(Lp F 2 volume)) ≤
      C *
        norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
            ↥(Lp F 2 volume))
Tactic: apply LinearMap.extendOfNorm_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))
have h : ∀ (x : 𝓢(E, F)),
  norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          x :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
          ↥(Lp F 2 volume))
Tactic: use 1