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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
have apply : EventuallyEq.{0, u_2} (β := E) atTop
  (fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
  fun (c : ℝ) ↦
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
    𝓕 (E := (w : V) → ℂ)
        (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
      f w
Tactic: apply A.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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪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) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
have h : ∀ (hc : 0 < c),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
        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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
⊢ EventuallyEq.{0, u_2} (β := E) atTop
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
        f w
have h : ∀ (c : ℝ) (hc : 0 < c),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
        f w)
Tactic: filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
        f w)
have J : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) volume
Tactic: have J : Integrable (fun w ↦ cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) :=
      GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) _ _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪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 B : Tendsto
  (fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
        f w)
  atTop (𝓝 (𝓕⁻ (𝓕 f) v))
Tactic: have B : Tendsto (fun (c : ℝ) ↦ (∫ w : V,
        𝓕 (fun w ↦ cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) w • f w)) atTop
      (𝓝 (𝓕⁻ (𝓕 f) v)) := by
    apply A.congr'
    filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
    have J : Integrable (fun w ↦ cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) :=
      GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) _ _
    simpa using (VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ V)
      Real.continuous_fourierChar continuous_inner J hf).symm
-- 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
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
⊢ EventuallyEq.{0, u_2} (β := E) atTop
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      𝓕 (E := (w : V) → ℂ)
          (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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),
  𝓕 (E := (w : V) → ℂ)
        (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) 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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ 𝓕 (E := (w : V) → ℂ)
        (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
      f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
have h : (((↑π : ℂ) / (↑c⁻¹ : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ))) •
    f w =
  (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
    f w
Tactic: rw [fourier_gaussian_innerProductSpace' (by simpa)]
-- 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
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ (((↑π : ℂ) / (↑c⁻¹ : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ))) •
      f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
have h : (↑π : ℂ) / (↑c⁻¹ : ℂ) = (↑π : ℂ) * (↑c : ℂ)
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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
h : (↑π : ℂ) / (↑c⁻¹ : ℂ) = (↑π : ℂ) * (↑c : ℂ)
⊢ (((↑π : ℂ) / (↑c⁻¹ : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ))) •
      f w =
    (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
        cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
      f w
have h₁ : -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ) =
  -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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        𝓕 (E := (w : V) → ℂ)
            (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) w •
          f w)
    atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
have h : HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 * (↑c : ℂ) =
  HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
Tactic: simp
-- 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)
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
have hφ : ∀ (x : V), 0 ≤ φ x
Tactic: apply tendsto_integral_comp_smul_smul_of_integrable'