awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v
have simp_rw : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫ : 𝕊) (f v))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
Tactic: simp_rw [fourierInv_eq, Circle.smul_def, Real.fourierChar_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫ : 𝕊) (f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
⊢ 𝓕⁻ f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v
have simp_rw₁ : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    HSMul.hSMul (α := ℂ) (↑((𝐞 : (a : ℝ) → 𝕊) ⟪v, w⟫) : ℂ) (f v))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    Complex.exp ((↑(2 * π * ⟪v, w⟫) : ℂ) * Complex.I) • f v)
Tactic: simp_rw [fourierInv_eq, Circle.smul_def, Real.fourierChar_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
have h : ∀ (y : V), 𝓕⁻ f y = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 y = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
have h : 𝓕 f (-y) = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
Tactic: rw [fourierInv_eq_fourier_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 (-y) = 𝓕 (E := (x : V) → E) (fun (x : V) ↦ f (-x)) y
have h : 𝓕 f ((LinearIsometryEquiv.neg ℝ : (a : V) → V) y) = 𝓕 (E := V → E) (f ∘ (⇑(LinearIsometryEquiv.neg ℝ) : (a : V) → V)) y
Tactic: change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
have rw : 𝓕 (E := (x : V) → E) fun (x : V) ↦ 𝓕 f (-x)
Tactic: rw [fourierInv_eq_fourier_comp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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) = 𝓕⁻ (𝓕 f)
have conv_rhs : 𝓕 (𝓕⁻ f) = 𝓕 (E := (x : V) → E) fun (x : V) ↦ 𝓕 f (-x)
Tactic: conv_rhs => rw [fourierInv_eq_fourier_comp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 : ℝ) → 𝕊) (-(v * w)) : 𝕊) (f v)
have simp_rw : 𝓕 f w =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-(w * v)) : 𝕊) (f v)
Tactic: simp_rw [mul_comm _ w]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ 𝓕 f w =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      Complex.exp ((↑(-2 * π * v * w) : ℂ) * Complex.I) • f v
have 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)
Tactic: simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ ‖𝓕 (↑(↑f : V →ₘ[volume] E) : V → E) x‖ ≤ ‖f‖
have 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‖
Tactic: rw [Real.fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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‖
have apply : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
    ‖HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)‖) ≤
  ‖f‖
Tactic: apply (norm_integral_le_integral_norm _).trans
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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) ↦
      ‖HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)‖) ≤
    ‖f‖
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦ ‖(↑(↑f : V →ₘ[volume] E) : V → E) a‖) ≤ ‖f‖
Tactic: simp_rw [Circle.norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ (⇑(Lp.fourierTransform (MemLp.toLp f hf)) : (a : V) → E) = 𝓕 f
have simp : 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) = 𝓕 f
Tactic: simp only [Lp.coe_fourierTransform]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) = 𝓕 f
have h : ∀ (x : V), 𝓕 (↑(↑(MemLp.toLp f hf) : V →ₘ[volume] E) : V → E) x = 𝓕 f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ fourierTransform (f + g) = fourierTransform f + fourierTransform g
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ Eq.{u_3 + 1} (α := E) ((fourierTransform (f + g) : (a : V) → E) x : E)
    ((fourierTransform f + fourierTransform g : (a : V) → E) x : E)
have 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))
Tactic: simp only [Lp.fourierTransform_apply, BoundedContinuousFunction.coe_add, Pi.add_apply,
          Real.fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ (@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))
have 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))
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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))
⊢ (@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))
have 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
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ (@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))
have 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
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ 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))
have 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)
Tactic: apply integral_congr_ae