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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
apply :
  Tendsto (fun (x : ℝ) ↦ -(↑x⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) atTop
    (𝓝 (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))
⊢ Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop
    (𝓝 (cexp (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v))

Tactic:
apply (Tendsto.cexp _).smul_const

Premises used: Filter.Tendsto.smul_const, Filter.Tendsto.cexp
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
⊢ Tendsto (fun (x : ℝ) ↦ -(↑x⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) atTop
    (𝓝 (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))

Tactic:
tendsto_inv_atTop_zero.ofReal.neg.mul_const _

Premises used: Filter.Tendsto.neg, tendsto_inv_atTop_zero, Filter.Tendsto.mul_const, Filter.Tendsto.ofReal
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
⊢ Tendsto (fun (x : ℝ) ↦ -(↑x⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) atTop
    (𝓝 (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))

Tactic:
exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _

Premises used: Filter.Tendsto.neg, tendsto_inv_atTop_zero, Filter.Tendsto.mul_const, Filter.Tendsto.ofReal
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (a : V) ↦
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)

Tactic:
fun_prop
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        (fun (n : ℝ) ↦
            AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
              (fun (a : V) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume)
          x}
      a
h₁ h₂ :
  ∀ (c : ℝ),
    AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (a : V) ↦ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume
⊢ ∀ᶠ (n : ℝ) in atTop,
    AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (a : V) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume

Tactic:
filter_upwards with c using
      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1

Premises used: And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
h : ∀ (hc : 0 ≤ c), ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) c →
    ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖

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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h : ∀ (c : ℝ) (hc : 0 ≤ c), ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖

Tactic:
filter_upwards [Ici_mem_atTop (0 : ℝ)] with c (hc : 0 ≤ c)

Premises used: Filter.Ici_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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
h : ∀ (v : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v‖ ≤ ‖f v‖
⊢ ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖

Tactic:
filter_upwards with v
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
h : ‖cexp (-((↑c : ℂ)⁻¹ * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))‖ * ‖f v‖ ≤ ‖f v‖
⊢ ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v‖ ≤ ‖f v‖

Tactic:
simp only [ofReal_inv, neg_mul, norm_smul]

Premises used: norm_smul, neg_mul, Complex.ofReal_inv
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ ‖f v‖
⊢ ‖cexp (-((↑c : ℂ)⁻¹ * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))‖ * ‖f v‖ ≤ ‖f v‖

Tactic:
norm_cast
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
rw : 1 * ‖f v‖
| ‖f v‖

Tactic:
rw [← one_mul (‖f v‖)]

Premises used: Norm.norm, one_mul
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ 1 * ‖f v‖
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ ‖f v‖

Tactic:
conv_rhs => rw [← one_mul (‖f v‖)]

Premises used: Norm.norm, one_mul
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ ≤ 1
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ 1 * ‖f v‖

Tactic:
gcongr
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
h : 0 ≤ c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ ≤ 1

Tactic:
simp only [norm_eq_abs, abs_exp, exp_le_one_iff, Left.neg_nonpos_iff]

Premises used: Left.neg_nonpos_iff, Real.exp_le_one_iff, Real.norm_eq_abs, Real.abs_exp
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ 0 ≤ c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
positivity
-- 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
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : V × V) ↦
    (((-innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) p.1 : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) p.2

Tactic:
have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg
-- 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
B :
  Continuous[instTopologicalSpaceProd, _] fun (p : V × V) ↦
    (((-innerₗ V : (a : V) → V →ₗ[ℝ] ℝ) p.1 : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) p.2
⊢ @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume

Tactic:
simpa using
        (VectorFourier.fourierIntegral_convergent_iff Real.continuous_fourierChar B v).2 h'f

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff, Real.continuous_fourierChar
-- 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
⊢ @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume

Tactic:
have : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • (𝓕 f) w) := by
      have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg
      simpa using
        (VectorFourier.fourierIntegral_convergent_iff Real.continuous_fourierChar B v).2 h'f
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
⊢ Tendsto.{0, u_2} (β := E)
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v_1 : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v_1‖ : ℂ) 2) •
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪v_1, v⟫ : Circle) (𝓕 f v_1))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v_1 : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪v_1, v⟫ : Circle) (𝓕 f v_1)))

Tactic:
tendsto_integral_cexp_sq_smul this

Premises used: Real.tendsto_integral_cexp_sq_smul
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
h :
  ∀ (c : ℝ) (w : V),
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w =
      cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2) •
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)
h₁ :
  𝓕⁻ (𝓕 f) v =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v_1 : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪v_1, v⟫ : Circle) (𝓕 f v_1)
⊢ 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))

Tactic:
convert! tendsto_integral_cexp_sq_smul this using 4 with c w

Premises used: Real.tendsto_integral_cexp_sq_smul
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
c : ℝ
w : V
h :
  cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ)) • 𝓕 f w =
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + (↑(2 * π * ⟪w, v⟫) : ℂ) * I) • 𝓕 f w
⊢ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪v, w⟫ : ℂ)) • 𝓕 f w =
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2) •
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)

Tactic:
rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]

Premises used: Complex.exp_add, smul_smul, Submonoid.smul_def, Real.fourierChar_apply, real_inner_comm
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
c : ℝ
w : V
h : 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = (↑(2 * π * ⟪w, v⟫) : ℂ) * I
⊢ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ)) • 𝓕 f w =
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + (↑(2 * π * ⟪w, v⟫) : ℂ) * I) • 𝓕 f w

Tactic:
congr 3
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
c : ℝ
w : V
h : 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = 2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = (↑(2 * π * ⟪w, v⟫) : ℂ) * I

Tactic:
simp only [ofReal_mul, ofReal_ofNat]

Premises used: Complex.ofReal_ofNat, Complex.ofReal_mul
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
c : ℝ
w : V
⊢ 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = 2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I

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
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
⊢ 𝓕⁻ (𝓕 f) v =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v_1 : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪v_1, v⟫ : Circle) (𝓕 f v_1)

Tactic:
simp [fourierInv_eq]

Premises used: Real.fourierInv_eq
-- 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
⊢ 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))

Tactic:
have A : Tendsto (fun (c : ℝ) ↦ (∫ w : V, cexp (- c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)
       • (𝓕 f) w)) atTop (𝓝 (𝓕⁻ (𝓕 f) v)) := by
    have : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • (𝓕 f) w) := by
      have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg
      simpa using
        (VectorFourier.fourierIntegral_convergent_iff Real.continuous_fourierChar B v).2 h'f
    convert! tendsto_integral_cexp_sq_smul this using 4 with c w
    · rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]
      congr 3
      simp only [ofReal_mul, ofReal_ofNat]
      ring
    · simp [fourierInv_eq]
-- 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))
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
⊢ 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:
apply A.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))
c : ℝ
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)
⊢ 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)

Tactic:
(hc : 0 < c)