awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (x : V),
    Eq.{u_2 + 1} (α := 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)) :
            (a : V) → E)
          x :
        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)) :
            (a : V) → E)
          x :
        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))) =
    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:
ext
-- 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 x : V
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m

Tactic:
have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
-- 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 x : V
this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
⊢ Eq.{u_2 + 1} (α := 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)) :
          (a : V) → E)
        x :
      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)) :
          (a : V) → E)
        x :
      E)

Tactic:
simp [this, innerSL_apply_apply ℝ]

Premises used: Real, innerSL_apply_apply
-- 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 :
  𝓕 (E := 𝓢(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) :
        𝓢(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))
⊢ 𝓕 (∂_{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
h :
  ∀ (x : V),
    Eq.{u_2 + 1} (α := E)
      ((𝓕 (E := 𝓢(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) :
                𝓢(V, E)) :
            (a : V) → E)
          x :
        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)) :
            (a : V) → E)
          x :
        E)
⊢ 𝓕 (E := 𝓢(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) :
        𝓢(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:
ext
-- 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 x : V
this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
⊢ Eq.{u_2 + 1} (α := E)
    ((𝓕 (E := 𝓢(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) :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      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)) :
          (a : V) → E)
        x :
      E)

Tactic:
simp [fourier_evalCLM_eq ℝ, fourier_fderivCLM_eq, this, innerSL_apply_apply ℝ]

Premises used: Real, innerSL_apply_apply, SchwartzMap.fourier_evalCLM_eq, SchwartzMap.fourier_fderivCLM_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
⊢ ∂_{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:
simp [fourierInv_apply_eq, lineDerivOp_compCLMOfContinuousLinearEquiv, lineDerivOp_fourier_eq]

Premises used: SchwartzMap.lineDerivOp_fourier_eq, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, SchwartzMap.fourierInv_apply_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
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m

Tactic:
fun_prop
-- 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
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m

Tactic:
have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
-- 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
this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
⊢ 𝓕⁻ (∂_{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:
simp [fourierInv_apply_eq, fourier_lineDerivOp_eq,
    smulLeftCLM_compCLMOfContinuousLinearEquiv ℂ this, Function.comp_def, smulLeftCLM_fun_neg this]

Premises used: SchwartzMap.fourier_lineDerivOp_eq, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, SchwartzMap.smulLeftCLM_fun_neg, SchwartzMap.fourierInv_apply_eq, Function.comp_def, Complex
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕 f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕 g : (a : V) → F) x : F))

Tactic:
simpa using VectorFourier.integral_bilin_fourierIntegral_eq_flip M (L := innerₗ V)
    continuous_fourierChar continuous_inner f.integrable g.integrable

Premises used: continuous_inner, VectorFourier.integral_bilin_fourierIntegral_eq_flip, Real.continuous_fourierChar, 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
inst_7 : CompleteSpace F
f : 𝓢(V, ℂ)
g : 𝓢(V, F)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HSMul.hSMul (α := ℂ) (β := F) ((𝓕 f : (a : V) → ℂ) ξ : ℂ) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HSMul.hSMul (α := ℂ) (β := F) ((f : (a : V) → ℂ) x : ℂ) ((𝓕 g : (a : V) → F) x : F))

Tactic:
integral_bilin_fourier_eq f g (.lsmul ℂ ℂ)

Premises used: SchwartzMap.integral_bilin_fourier_eq, Complex, ContinuousLinearMap.lsmul
-- 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
f g : 𝓢(V, ℂ)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((𝓕 f : (a : V) → ℂ) ξ : ℂ) ((g : (a : V) → ℂ) ξ : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : V) → ℂ) x : ℂ) ((𝓕 g : (a : V) → ℂ) x : ℂ))

Tactic:
integral_bilin_fourier_eq f g (.mul ℂ ℂ)

Premises used: SchwartzMap.integral_bilin_fourier_eq, ContinuousLinearMap.mul, Complex
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕⁻ f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕 (𝓕⁻ g) : (a : V) → F) x : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕 (𝓕⁻ f) : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((𝓕⁻ g : (a : V) → F) ξ : F))

Tactic:
(integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm

Premises used: SchwartzMap.integral_bilin_fourier_eq, FourierTransformInv.fourierInv, Eq.symm
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
h : ∀ (x : V), g = 𝓕 (𝓕⁻ g)
h₁ : ∀ (x : V), f = 𝓕 (𝓕⁻ f)
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕⁻ f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕⁻ g : (a : V) → F) x : F))

Tactic:
convert! (integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm

Premises used: SchwartzMap.integral_bilin_fourier_eq, FourierTransformInv.fourierInv, Eq.symm
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
x : V
⊢ g = 𝓕 (𝓕⁻ g)

Tactic:
(FourierTransform.fourier_fourierInv_eq g).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
x : V
⊢ g = 𝓕 (𝓕⁻ g)

Tactic:
exact (FourierTransform.fourier_fourierInv_eq g).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
x : V
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
(FourierTransform.fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
x : V
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
exact (FourierTransform.fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
inst_7 : CompleteSpace F
f : 𝓢(V, ℂ)
g : 𝓢(V, F)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HSMul.hSMul (α := ℂ) (β := F) ((𝓕⁻ f : (a : V) → ℂ) ξ : ℂ) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HSMul.hSMul (α := ℂ) (β := F) ((f : (a : V) → ℂ) x : ℂ) ((𝓕⁻ g : (a : V) → F) x : F))

Tactic:
integral_bilin_fourierInv_eq f g (.lsmul ℂ ℂ)

Premises used: SchwartzMap.integral_bilin_fourierInv_eq, Complex, ContinuousLinearMap.lsmul
-- 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
f g : 𝓢(V, ℂ)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((𝓕⁻ f : (a : V) → ℂ) ξ : ℂ) ((g : (a : V) → ℂ) ξ : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : V) → ℂ) x : ℂ) ((𝓕⁻ g : (a : V) → ℂ) x : ℂ))

Tactic:
integral_bilin_fourierInv_eq f g (.mul ℂ ℂ)

Premises used: SchwartzMap.integral_bilin_fourierInv_eq, ContinuousLinearMap.mul, Complex
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕 f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕⁻ g : (a : V) → F) x : F))

Tactic:
simpa [fourierInv_coe] using VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip M
    (L := innerₗ V) continuous_fourierChar continuous_inner f.integrable g.integrable

Premises used: VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, continuous_inner, SchwartzMap.fourierInv_coe, Real.continuous_fourierChar, SchwartzMap.integrable
-- 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 : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕 f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((𝓕 g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) x : F))

Tactic:
simpa using integral_sesq_fourier_eq f (𝓕 g) M

Premises used: SchwartzMap.integral_sesq_fourier_eq, FourierTransform.fourier
-- 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
x : V
rw :
  ‖𝓕 (E := (a : V) → F) (⇑f : (a : V) → F) x‖ =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
rw₁ rw₂ :
  Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F)) =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
⊢ Norm.norm.{u_4} (E := F) ((𝓕 f : (a : V) → F) x : F) =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))

Tactic:
rw [fourier_coe, Real.fourier_eq]

Premises used: Real.fourier_eq, SchwartzMap.fourier_coe
-- 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
x : V
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      ‖HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F)‖) =
    Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)

Tactic:
simp [norm_toLp_one]

Premises used: SchwartzMap.norm_toLp_one
-- 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ 0 ≤ Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)

Tactic:
positivity
-- 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
rw :
  ∀ (x : V),
    Norm.norm.{u_4} (E := F) (((𝓕 f).toBoundedContinuousFunction : (a : V) → F) x : F) ≤
      Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)
⊢ ‖(𝓕 f).toBoundedContinuousFunction‖ ≤ Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)

Tactic:
rw [BoundedContinuousFunction.norm_le (by positivity)]

Premises used: BoundedContinuousFunction.norm_le
-- 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
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V),
    Norm.norm.{u_4} (E := F) (((𝓕 f).toBoundedContinuousFunction : (a : V) → F) x : F) ≤
      Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)

Tactic:
simpa using norm_fourier_apply_le_toLp_one f

Premises used: SchwartzMap.norm_fourier_apply_le_toLp_one