awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n_1 : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn_1 : (↑n_1 : ℕ∞) ≤ N
x : ℝ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f) volume
have rw : @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace
  ((⇑(ContinuousMultilinearMap.piFieldEquiv ℝ (Fin n) E) :
      (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ ℝ) E) ∘
    iteratedDeriv n f)
  volume
Tactic: rw [iteratedFDeriv_eq_equiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
⊢ 𝓕 (iteratedDeriv n f) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
have A : ∀ (n : ℕ),
  (↑n : ℕ∞) ≤ N →
    @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f) volume
Tactic: have A : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) := by
    intro n hn
    rw [iteratedFDeriv_eq_equiv_comp]
    exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable _ _ _ _ measurableSpace (iteratedDeriv n f) volume
hn : (↑n : ℕ∞) ≤ N
x : ℝ
A :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) E) _ _ _ measurableSpace (iteratedFDeriv ℝ n f)
        volume
⊢ 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ iteratedDeriv n f x) x = (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
have h : ((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n : (a : (i : Fin n) → ℝ) → E) fun (x : Fin n) ↦ 1) =
  (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ n • 𝓕 f x
Tactic: simp_rw [iteratedDeriv, ← fourier_continuousMultilinearMap_apply (A n hn),
    fourier_iteratedFDeriv hf A hn]
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ Tendsto.{0, u_2} (β := E)
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v)
    atTop (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ f v))
have apply : ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))
Tactic: apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
apply : ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))
⊢ Tendsto.{0, u_2} (β := E)
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v)
    atTop (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ f v))
have apply₁ : ∀ᶠ (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: apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
apply : ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))
apply₁ :
  ∀ᶠ (n : ℝ) in atTop,
    AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (a : V) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume
⊢ Tendsto.{0, u_2} (β := E)
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v)
    atTop (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ f v))
have apply₂ : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
Tactic: apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ ∀ᵐ (a : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) atTop (𝓝 (f a))
have h : ∀ (v : V), Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop (𝓝 (f v))
Tactic: filter_upwards with 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
⊢ Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop (𝓝 (f v))
have h : Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop
  (𝓝 (cexp (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v))
Tactic: nth_rewrite 2 [show f v = cexp (- (0 : ℝ) * ‖v‖ ^ 2) • f v by 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
⊢ Tendsto (fun (n : ℝ) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v) atTop
    (𝓝 (cexp (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v))
have apply : Tendsto (fun (x : ℝ) ↦ -(↑x⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) atTop
  (𝓝 (-(↑0 : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))
Tactic: apply (Tendsto.cexp _).smul_const
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f 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
have 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
Tactic: filter_upwards with c using
      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1
-- 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
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
⊢ ∀ᶠ (n : ℝ) in atTop,
    AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (a : V) ↦ cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a) volume
have h₁ : ∀ (a : ℝ),
  AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (a_1 : V) ↦ cexp (-(↑a⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a_1‖ : ℂ) 2) • f a_1) volume
Tactic: filter_upwards with c using
      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) c →
    ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
have h : ∀ (hc : 0 ≤ c), ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-(↑n⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
have h : ∀ (c : ℝ) (hc : 0 ≤ c), ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
Tactic: filter_upwards [Ici_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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
⊢ ∀ᵐ (a : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2) • f a‖ ≤ ‖f a‖
have h : ∀ (v : V), ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v‖ ≤ ‖f v‖
Tactic: filter_upwards with 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) • f v‖ ≤ ‖f v‖
have h : ‖cexp (-((↑c : ℂ)⁻¹ * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))‖ * ‖f v‖ ≤ ‖f v‖
Tactic: simp only [ofReal_inv, neg_mul, norm_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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-((↑c : ℂ)⁻¹ * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))‖ * ‖f v‖ ≤ ‖f v‖
have h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ ‖f v‖
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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
| ‖f v‖
have rw : 1 * ‖f v‖
Tactic: rw [← one_mul (‖f 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ ‖f v‖
have h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ 1 * ‖f v‖
Tactic: conv_rhs => rw [← one_mul (‖f 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ * ‖f v‖ ≤ 1 * ‖f v‖
have h : ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ ≤ 1
Tactic: gcongr
-- 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
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2))‖ ≤ 1
have h : 0 ≤ c⁻¹ * HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: simp only [norm_eq_abs, abs_exp, exp_le_one_iff, Left.neg_nonpos_iff]
-- 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
⊢ @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
have B : 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
-- 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
⊢ 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))
have this : @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
-- 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
this :
  @Integrable.{u_2, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (w : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪w, v⟫ : Circle) (𝓕 f w)) volume
⊢ 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))
have 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)
Tactic: convert! tendsto_integral_cexp_sq_smul this using 4 with c 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
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)
⊢ 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))
have h₁ : 𝓕⁻ (𝓕 f) v =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v_1 : V) ↦
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) ⟪v_1, v⟫ : Circle) (𝓕 f v_1)
Tactic: convert! tendsto_integral_cexp_sq_smul this using 4 with c 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
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
⊢ 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)
have 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
Tactic: rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_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
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
⊢ cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ)) • 𝓕 f w =
    cexp (-(↑c⁻¹ : ℂ) * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 + (↑(2 * π * ⟪w, v⟫) : ℂ) * I) • 𝓕 f w
have h : 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = (↑(2 * π * ⟪w, v⟫) : ℂ) * I
Tactic: congr 3
-- 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
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
have h : 2 * (↑π : ℂ) * I * (↑⟪w, v⟫ : ℂ) = 2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I
Tactic: simp only [ofReal_mul, ofReal_ofNat]
-- 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
⊢ 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 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))
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]