awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
this :
  (p.1 + integrablePower.{u_3} (E := V) volume, p.2) ∈
    Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)
⊢ LE.le (α := ℝ)
    ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)

Tactic:
apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)

Premises used: Seminorm.le_def, Iff.mp, Finset.le_sup
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      HMul.hMul (β := ℝ)
        ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ) =
    (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
      (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
            (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                    (schwartzSeminormFamily 𝕜 V E) :
                  (a : 𝓢(V, E)) → ℝ)
                f :
              ℝ)))

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
⊢ (⇑(𝓕 f) : (a : V) → E) = 𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)

Tactic:
rfl

Premises used: VectorFourier.fourierIntegral, rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
⊢ ((fourierTransformCLM 𝕜 : 𝓢(V, E) →L[𝕜] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f = 𝓕 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
h : ∀ (x : V), (𝓕⁻ f : (a : V) → E) x = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E) x
⊢ (⇑(𝓕⁻ f) : (a : V) → E) = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ (𝓕⁻ f : (a : V) → E) x = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E) x

Tactic:
(fourierInv_eq_fourier_neg f x).symm

Premises used: Real.fourierInv_eq_fourier_neg, VectorFourier.fourierIntegral, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ (𝓕⁻ f : (a : V) → E) x = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E) x

Tactic:
exact (fourierInv_eq_fourier_neg f x).symm

Premises used: Real.fourierInv_eq_fourier_neg, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
⊢ 𝓕⁻ f = (compCLMOfContinuousLinearEquiv ℂ (↑(LinearIsometryEquiv.neg ℝ) : V ≃L[ℝ] V) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
h : ∀ (x : V), Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕⁻ (E := (a : V) → E) (⇑(𝓕 f) : (a : V) → E) x = (f : (a : V) → E) x
h₁ : 𝓕⁻ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
h₂ h₃ : Eq.{u_2 + 1} (α := E) ((f : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)

Tactic:
rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
      (𝓕 f).integrable]

Premises used: SchwartzMap.continuous, Continuous.fourierInv_fourier_eq, SchwartzMap.fourier_coe, SchwartzMap.fourierInv_coe, SchwartzMap.integrable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
h : ∀ (x : V), Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕 (E := (a : V) → E) (⇑(𝓕⁻ f) : (a : V) → E) x = (f : (a : V) → E) x
h₁ : 𝓕 (𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
h₂ h₃ : Eq.{u_2 + 1} (α := E) ((f : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)

Tactic:
rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable]

Premises used: SchwartzMap.continuous, SchwartzMap.fourier_coe, SchwartzMap.fourierInv_coe, Continuous.fourier_fourierInv_eq, SchwartzMap.integrable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
𝕜' : Type u_4
inst_5 : NormedField 𝕜'
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
G : Type u_6
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℂ G
inst_10 : NormedSpace 𝕜' G
inst_11 : SMulCommClass ℝ 𝕜' G
f : 𝓢(V, F →L[ℝ] G)
m : F
h :
  ∀ (x : V),
    Eq.{u_6 + 1} (α := G)
      ((𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) : (a : V) → G)
          x :
        G)
      ((((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f) : 𝓢(V, G)) : (a : V) → G) x : G)
⊢ 𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) =
    (SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
𝕜' : Type u_4
inst_5 : NormedField 𝕜'
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
G : Type u_6
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℂ G
inst_10 : NormedSpace 𝕜' G
inst_11 : SMulCommClass ℝ 𝕜' G
f : 𝓢(V, F →L[ℝ] G)
m : F
x : V
⊢ Eq.{u_6 + 1} (α := G)
    ((𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) : (a : V) → G) x :
      G)
    ((((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f) : 𝓢(V, G)) : (a : V) → G) x : G)

Tactic:
(fourier_continuousLinearMap_apply f.integrable).symm

Premises used: Real.fourier_continuousLinearMap_apply, VectorFourier.fourierIntegral, SchwartzMap.integrable, Eq.symm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
𝕜' : Type u_4
inst_5 : NormedField 𝕜'
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
G : Type u_6
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℂ G
inst_10 : NormedSpace 𝕜' G
inst_11 : SMulCommClass ℝ 𝕜' G
f : 𝓢(V, F →L[ℝ] G)
m : F
x : V
⊢ Eq.{u_6 + 1} (α := G)
    ((𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) : (a : V) → G) x :
      G)
    ((((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f) : 𝓢(V, G)) : (a : V) → G) x : G)

Tactic:
exact (fourier_continuousLinearMap_apply f.integrable).symm

Premises used: Real.fourier_continuousLinearMap_apply, SchwartzMap.integrable, Eq.symm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
h :
  ∀ (x : V),
    Eq (α := V →L[ℝ] E)
      ((((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) : 𝓢(V, V →L[ℝ] E)) : (a : V) → V →L[ℝ] E) x :
        V →L[ℝ] E)
      ((𝓕
              (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
                (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                  𝓢(V, V →L[ℝ] E))) :
            (a : V) → V →L[ℝ] E)
          x :
        V →L[ℝ] E)
⊢ (fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
          𝓢(V, V →L[ℝ] E)))

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x : V
h :
  fderiv ℝ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x =
    𝓕 (E := (v : V) → V →L[ℝ] E) (VectorFourier.fourierSMulRight (innerSL ℝ) (⇑f : (a : V) → E)) x
⊢ Eq (α := V →L[ℝ] E)
    ((((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) : 𝓢(V, V →L[ℝ] E)) : (a : V) → V →L[ℝ] E) x :
      V →L[ℝ] E)
    ((𝓕
            (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
              (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                𝓢(V, V →L[ℝ] E))) :
          (a : V) → V →L[ℝ] E)
        x :
      V →L[ℝ] E)

Tactic:
change fderiv ℝ (𝓕 ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) f) x

Premises used: VectorFourier.fourierSMulRight, Real, innerSL, fderiv, FourierTransform.fourier, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x : V
h :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ ‖v‖ * Norm.norm.{u_2} (E := E) ((f : (a : V) → E) v : E)) volume
⊢ fderiv ℝ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x =
    𝓕 (E := (v : V) → V →L[ℝ] E) (VectorFourier.fourierSMulRight (innerSL ℝ) (⇑f : (a : V) → E)) x

Tactic:
rw [fderiv_fourier f.integrable]

Premises used: Real.fderiv_fourier, SchwartzMap.integrable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ ‖v‖ * Norm.norm.{u_2} (E := E) ((f : (a : V) → E) v : E)) volume

Tactic:
simpa using f.integrable_pow_mul volume 1

Premises used: MeasureTheory.MeasureSpace.volume, SchwartzMap.integrable_pow_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
h :
  ∀ (x m : V),
    Eq.{u_2 + 1} (α := E)
      ((((𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) :
                  (a : V) → V →L[ℝ] E)
                x :
              V →L[ℝ] E) :
            (a : V) → E)
          m :
        E)
      ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                    (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                        (𝓕 f) :
                      𝓢(V, V →L[ℝ] E)) :
                  (a : V) → V →L[ℝ] E)
                x :
              V →L[ℝ] E) :
            (a : V) → E)
          m :
        E)
⊢ 𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) =
    HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
      (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) :
        𝓢(V, V →L[ℝ] E))

Tactic:
ext x m
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x m : V
h :
  Eq.{u_2 + 1} (α := E) ((𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ (⇑f : (a : V) → E)) x : (a : V) → E) m : E)
    ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                  (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                      (𝓕 f) :
                    𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
⊢ Eq.{u_2 + 1} (α := E)
    ((((𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
    ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                  (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                      (𝓕 f) :
                    𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)

Tactic:
change 𝓕 (fderiv ℝ ⇑f) x m = _

Premises used: Real, fderiv, FourierTransform.fourier, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x m : V
⊢ Eq.{u_2 + 1} (α := E) ((𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ (⇑f : (a : V) → E)) x : (a : V) → E) m : E)
    ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                  (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                      (𝓕 f) :
                    𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)

Tactic:
simp [fourier_fderiv f.integrable f.differentiable (fderivCLM ℝ V E f).integrable,
    innerSL_apply_apply ℝ, fourier_coe]

Premises used: Real, innerSL_apply_apply, SchwartzMap.differentiable, SchwartzMap.fderivCLM, Real.fourier_fderiv, SchwartzMap.fourier_coe, SchwartzMap.integrable, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
change :
  (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
      ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
⊢ ∂_{m} (𝓕 f) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))

Tactic:
change SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E (𝓕 f)) = _

Premises used: Real, SchwartzMap.fderivCLM, SchwartzMap.evalCLM, FourierTransform.fourier, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
rw :
  𝓕 (E := 𝓢(V, E))
      ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
          (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
            (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
              𝓢(V, V →L[ℝ] E))) :
        𝓢(V, E)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
⊢ (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
      ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))

Tactic:
rw [fderivCLM_fourier_eq, ← fourier_evalCLM_eq]

Premises used: SchwartzMap.fourier_evalCLM_eq, SchwartzMap.fderivCLM_fourier_eq
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
e_a :
  (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
      (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
          𝓢(V, V →L[ℝ] E))) =
    HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E))
⊢ 𝓕 (E := 𝓢(V, E))
      ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
          (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
            (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
              𝓢(V, V →L[ℝ] E))) :
        𝓢(V, E)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))

Tactic:
congr