awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕 (E := W → E) (f ∘ (⇑A : (a : W) → V)) w = 𝓕 f ((A : (a : W) → V) w)

Tactic:
simp only [fourier_eq, ← A.inner_map_map, Function.comp_apply,
    ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]

Premises used: LinearIsometryEquiv.toHomeomorph, MeasureTheory.MeasurePreserving.integral_comp, Homeomorph.measurableEmbedding, LinearIsometryEquiv.measurePreserving, Real.fourier_eq, LinearIsometryEquiv.inner_map_map, Function.comp_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕⁻ f w = 𝓕 f (-w)

Tactic:
simp [fourier_eq, fourierInv_eq]

Premises used: Real.fourier_eq, Real.fourierInv_eq
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
h : ∀ (y : V), 𝓕⁻ f y = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
⊢ 𝓕⁻ f = 𝓕 (E := (x : V) → E) fun (x : V) ↦ f (-x)

Tactic:
ext y
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
y : V
h : 𝓕 f (-y) = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
⊢ 𝓕⁻ f y = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y

Tactic:
rw [fourierInv_eq_fourier_neg]

Premises used: Real.fourierInv_eq_fourier_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
y : V
h :
  𝓕 f ((LinearIsometryEquiv.neg ℝ : (a : V) → V) y) =
    𝓕 (E := V → E) (f ∘ (⇑(LinearIsometryEquiv.neg ℝ) : (a : V) → V)) y
⊢ 𝓕 f (-y) = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y

Tactic:
change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y

Premises used: Real, Function.comp, FourierTransform.fourier, LinearIsometryEquiv.neg, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f ((LinearIsometryEquiv.neg ℝ : (a : V) → V) y) =
    𝓕 (E := V → E) (f ∘ (⇑(LinearIsometryEquiv.neg ℝ) : (a : V) → V)) y

Tactic:
(fourier_comp_linearIsometry _ _ _).symm

Premises used: Real.fourier_comp_linearIsometry, Eq.symm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f ((LinearIsometryEquiv.neg ℝ : (a : V) → V) y) =
    𝓕 (E := V → E) (f ∘ (⇑(LinearIsometryEquiv.neg ℝ) : (a : V) → V)) y

Tactic:
exact (fourier_comp_linearIsometry _ _ _).symm

Premises used: Real.fourier_comp_linearIsometry, Eq.symm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
rw : 𝓕 (E := (x : V) → E) fun (x : V) ↦ 𝓕 f (-x)
| 𝓕⁻ (𝓕 f)

Tactic:
rw [fourierInv_eq_fourier_comp_neg]

Premises used: Real.fourierInv_eq_fourier_comp_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
conv_rhs : 𝓕 (𝓕⁻ f) = 𝓕 (E := (x : V) → E) fun (x : V) ↦ 𝓕 f (-x)
⊢ 𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f)

Tactic:
conv_rhs => rw [fourierInv_eq_fourier_comp_neg]

Premises used: Real.fourierInv_eq_fourier_comp_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕 (E := (x : V) → E) fun (x : V) ↦ 𝓕 f (-x)

Tactic:
simp_rw [← fourierInv_eq_fourier_neg]

Premises used: Real.fourierInv_eq_fourier_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕⁻ (E := W → E) (f ∘ (⇑A : (a : W) → V)) w = 𝓕⁻ f ((A : (a : W) → V) w)

Tactic:
simp [fourierInv_eq_fourier_neg, fourier_comp_linearIsometry]

Premises used: Real.fourierInv_eq_fourier_neg, Real.fourier_comp_linearIsometry
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
w : ℝ
simp_rw :
  𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(w * v)) : 𝕊) (f v)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(v * w)) : 𝕊) (f v)

Tactic:
simp_rw [mul_comm _ w]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(w * v)) : 𝕊) (f v)

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
w : ℝ
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(v * w)) : 𝕊) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v)
simp_rw₁ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := ℂ) (↑((𝐞 : (a : ℝ) → 𝕊) (-(v * w))) : ℂ) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v)
simp_rw₂ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(2 * π * -(v * w)) : ℂ) * Complex.I) • f v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v)
simp_rw₃ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-(2 * π * (v * w))) : ℂ) * Complex.I) • f v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v)
simp_rw₄ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-(2 * π * (v * w))) : ℂ) * Complex.I) • f v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-(2 * π * v * w)) : ℂ) * Complex.I) • f v)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v

Tactic:
simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]

Premises used: mul_assoc, Real.fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, neg_mul, mul_neg
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
f : V → F →L[ℝ] E
a : F
v : V
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ (𝓕 f v : (a : F) → E) a = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ (f x : (a : F) → E) a) v

Tactic:
fourierIntegral_continuousLinearMap_apply' (L := innerSL ℝ) hf

Premises used: MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, Real.fourierIntegral_continuousLinearMap_apply', starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
ι : Type u_4
inst_7 : Fintype ι
M : ι → Type u_5
inst_8 : (i : ι) → NormedAddCommGroup (M i)
inst_9 : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
v : V
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ (𝓕 f v : (a : (i : ι) → M i) → E) m = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ (f x : (a : (i : ι) → M i) → E) m) v

Tactic:
fourierIntegral_continuousMultilinearMap_apply' (L := innerSL ℝ) hf

Premises used: MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ, Real.fourierIntegral_continuousMultilinearMap_apply'
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
rw :
  Norm.norm.{u_3} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v)) ≤
    ‖f‖
⊢ ‖𝓕 (↑(↑f : V →ₘ[volume] E) : V → E) x‖ ≤ ‖f‖

Tactic:
rw [Real.fourier_eq]

Premises used: Real.fourier_eq
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
apply :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)‖) ≤
    ‖f‖
⊢ Norm.norm.{u_3} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v)) ≤
    ‖f‖

Tactic:
apply (norm_integral_le_integral_norm _).trans

Premises used: MeasureTheory.norm_integral_le_integral_norm, LE.le.trans
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦ ‖(↑(↑f : V →ₘ[volume] E) : V → E) a‖) ≤ ‖f‖
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      ‖HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)‖) ≤
    ‖f‖

Tactic:
simp_rw [Circle.norm_smul]

Premises used: Circle.norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦ ‖(↑(↑f : V →ₘ[volume] E) : V → E) a‖) ≤ ‖f‖

Tactic:
(L1.norm_eq_integral_norm f).symm.le

Premises used: Eq.le, Eq.symm, MeasureTheory.L1.norm_eq_integral_norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦ ‖(↑(↑f : V →ₘ[volume] E) : V → E) a‖) ≤ ‖f‖

Tactic:
exact (L1.norm_eq_integral_norm f).symm.le

Premises used: Eq.le, Eq.symm, MeasureTheory.L1.norm_eq_integral_norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ (⇑(fourierTransform f) : (a : V) → E) = 𝓕 (↑(↑f : V →ₘ[volume] E) : V → E)

Tactic:
rfl

Premises used: VectorFourier.fourierIntegral, rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ (fourierTransform f : (a : V) → E) x = 𝓕 (↑(↑f : V →ₘ[volume] E) : V → E) x

Tactic:
rfl

Premises used: VectorFourier.fourierIntegral, rfl
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
hf : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 1 volume
simp : 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) = 𝓕 f
⊢ (⇑(Lp.fourierTransform (MemLp.toLp f hf)) : (a : V) → E) = 𝓕 f

Tactic:
simp only [Lp.coe_fourierTransform]

Premises used: Real.Lp.coe_fourierTransform
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
hf : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 1 volume
h : ∀ (x : V), 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) x = 𝓕 f x
⊢ 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) = 𝓕 f

Tactic:
ext x
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
hf : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 1 volume
x : V
⊢ 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) x = 𝓕 f x

Tactic:
(Real.fourier_congr_ae hf.coeFn_toLp) x

Premises used: MeasureTheory.MemLp.coeFn_toLp, Real.fourier_congr_ae
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : FiniteDimensional ℝ V
f : V → E
hf : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 1 volume
x : V
⊢ 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) x = 𝓕 f x

Tactic:
exact (Real.fourier_congr_ae hf.coeFn_toLp) x

Premises used: MeasureTheory.MemLp.coeFn_toLp, Real.fourier_congr_ae
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
h :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := E) ((fourierTransform (f + g) : (a : V) → E) x : E)
      ((fourierTransform f + fourierTransform g : (a : V) → E) x : E)
⊢ fourierTransform (f + g) = fourierTransform f + fourierTransform g

Tactic:
ext x
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x : V
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) v)) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) v))
⊢ Eq.{u_3 + 1} (α := E) ((fourierTransform (f + g) : (a : V) → E) x : E)
    ((fourierTransform f + fourierTransform g : (a : V) → E) x : E)

Tactic:
simp only [Lp.fourierTransform_apply, BoundedContinuousFunction.coe_add, Pi.add_apply,
          Real.fourier_eq]

Premises used: Real.Lp.fourierTransform_apply, BoundedContinuousFunction.coe_add, Real.fourier_eq, Pi.add_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x : V
h :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a) +
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) a))
h₁ :
  @Integrable.{u_3, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v)) volume
h₂ :
  @Integrable.{u_3, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) v)) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) v)) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) v))

Tactic:
rw [← integral_add]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
V : Type u_1
W : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : MeasurableSpace V
inst_5 : BorelSpace V
inst_6 : NormedAddCommGroup W
inst_7 : InnerProductSpace ℝ W
inst_8 : MeasurableSpace W
inst_9 : BorelSpace W
inst_10 : FiniteDimensional ℝ W
inst_11 : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x : V
h :
  EventuallyEq.{u_1, u_3} (β := E) (ae (F := Measure V) volume)
    (fun (a : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) a))
    fun (a : V) ↦
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a) +
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) a)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a) +
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) a))

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae