awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Inversion
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))
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)
⊢ 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:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.Inversion
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
⊢ 0 < (↑c⁻¹ : ℂ).re

Tactic:
simpa
-- Module: Mathlib.Analysis.Fourier.Inversion
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
⊢ @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) _ _
-- Module: Mathlib.Analysis.Fourier.Inversion
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
J :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ))) volume
⊢ 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:
simpa using (VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ V)
      Real.continuous_fourierChar continuous_inner J hf).symm

Premises used: continuous_inner, Real.continuous_fourierChar, VectorFourier.integral_fourierIntegral_smul_eq_flip, Eq.symm
-- Module: Mathlib.Analysis.Fourier.Inversion
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))

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
-- Module: Mathlib.Analysis.Fourier.Inversion
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))
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
⊢ 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))

Tactic:
apply B.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Fourier.Inversion
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 : ℝ
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)
⊢ 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)

Tactic:
(hc : 0 < c)
-- Module: Mathlib.Analysis.Fourier.Inversion
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))
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)
⊢ 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:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.Inversion
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
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
⊢ 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:
congr with w
-- Module: Mathlib.Analysis.Fourier.Inversion
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
⊢ 0 < (↑c⁻¹ : ℂ).re

Tactic:
simpa
-- Module: Mathlib.Analysis.Fourier.Inversion
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⁻¹ : ℂ)) ^ 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
⊢ 𝓕 (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:
rw [fourier_gaussian_innerProductSpace' (by simpa)]

Premises used: fourier_gaussian_innerProductSpace'
-- Module: Mathlib.Analysis.Fourier.Inversion
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 : ℂ)
h₁ :
  -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
⊢ (((↑π : ℂ) / (↑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:
congr
-- Module: Mathlib.Analysis.Fourier.Inversion
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⁻¹ : ℂ) = (↑π : ℂ) * (↑c : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Inversion
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 :
  HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 * (↑c : ℂ) =
    HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2
⊢ -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2 / (↑c⁻¹ : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Inversion
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

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.Inversion
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)
hφ : ∀ (x : V), 0 ≤ φ x
h'φ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ φ x) 1
h : Tendsto (β := ℝ) (fun (x : V) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'g : ContinuousAt f v
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))

Tactic:
apply tendsto_integral_comp_smul_smul_of_integrable'

Premises used: tendsto_integral_comp_smul_smul_of_integrable'