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
f g : ↥(Lp E 1 volume)
x : V
h :
  ∀ (x_1 : V)
    (h₁ :
      (↑(↑(f + g) : V →ₘ[volume] E) : V → E) x_1 =
        ((↑(↑f : V →ₘ[volume] E) : V → E) + (↑(↑g : V →ₘ[volume] E) : V → E)) x_1),
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x_1, x⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) x_1) =
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x_1, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x_1) +
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x_1, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) x_1)
⊢ 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:
filter_upwards [Lp.coeFn_add f g] with x h₁

Premises used: MeasureTheory.Lp.coeFn_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_1 x : V
h₁ : (↑(↑(f + g) : V →ₘ[volume] E) : V → E) x = ((↑(↑f : V →ₘ[volume] E) : V → E) + (↑(↑g : V →ₘ[volume] E) : V → E)) x
h :
  HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊)
      (((↑(↑f : V →ₘ[volume] E) : V → E) + (↑(↑g : V →ₘ[volume] E) : V → E)) x) =
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x) +
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) x)
⊢ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑(f + g) : V →ₘ[volume] E) : V → E) x) =
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x) +
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) x)

Tactic:
rw [h₁]
-- 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_1 x : V
h₁ : (↑(↑(f + g) : V →ₘ[volume] E) : V → E) x = ((↑(↑f : V →ₘ[volume] E) : V → E) + (↑(↑g : V →ₘ[volume] E) : V → E)) x
⊢ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊)
      (((↑(↑f : V →ₘ[volume] E) : V → E) + (↑(↑g : V →ₘ[volume] E) : V → E)) x) =
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x) +
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) x)

Tactic:
simp
-- 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 : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑f : V →ₘ[volume] E) : V → E) volume
⊢ @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 [Real.fourierIntegral_convergent_iff]

Premises used: Real.fourierIntegral_convergent_iff
-- 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
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑f : V →ₘ[volume] E) : V → E) volume

Tactic:
L1.integrable_coeFn f

Premises used: MeasureTheory.L1.integrable_coeFn
-- 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
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑f : V →ₘ[volume] E) : V → E) volume

Tactic:
exact L1.integrable_coeFn f

Premises used: MeasureTheory.L1.integrable_coeFn
-- 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 : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑g : V →ₘ[volume] E) : V → E) volume
⊢ @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 [Real.fourierIntegral_convergent_iff]

Premises used: Real.fourierIntegral_convergent_iff
-- 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
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑g : V →ₘ[volume] E) : V → E) volume

Tactic:
L1.integrable_coeFn g

Premises used: MeasureTheory.L1.integrable_coeFn
-- 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
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑g : V →ₘ[volume] E) : V → E) volume

Tactic:
exact L1.integrable_coeFn g

Premises used: MeasureTheory.L1.integrable_coeFn
-- 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
c : ℂ
f : ↥(Lp E 1 volume)
h :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := E) ((fourierTransform (c • f) : (a : V) → E) x : E)
      ((HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (fourierTransform f) : (a : V) → E) x : E)
⊢ fourierTransform (c • f) = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (fourierTransform f)

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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) v)) =
    HSMul.hSMul (α := ℂ) (β := E) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v))
⊢ Eq.{u_3 + 1} (α := E) ((fourierTransform (c • f) : (a : V) → E) x : E)
    ((HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (fourierTransform f) : (a : V) → E) x : E)

Tactic:
simp only [Lp.fourierTransform_apply, BoundedContinuousFunction.coe_smul, Real.fourier_eq]

Premises used: BoundedContinuousFunction.coe_smul, Real.Lp.fourierTransform_apply, 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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
h :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
        (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) v)) =
    HSMul.hSMul (α := ℂ) (β := E) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v))

Tactic:
rw [← integral_smul]

Premises used: MeasureTheory.integral_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
c : ℂ
f : ↥(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⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) a))
    fun (a : V) ↦
    HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a))
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : V) ↦
      HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
        (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a)))

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
h :
  ∀ (x_1 : V) (h : (↑(↑(c • f) : V →ₘ[volume] E) : V → E) x_1 = (c • (↑(↑f : V →ₘ[volume] E) : V → E)) x_1),
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x_1, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) x_1) =
      HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
        (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x_1, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x_1))
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae (F := Measure V) volume)
    (fun (a : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) a))
    fun (a : V) ↦
    HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪a, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) a))

Tactic:
filter_upwards [Lp.coeFn_smul c f] with x h

Premises used: MeasureTheory.Lp.coeFn_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
c : ℂ
f : ↥(Lp E 1 volume)
x_1 x : V
h : (↑(↑(c • f) : V →ₘ[volume] E) : V → E) x = (c • (↑(↑f : V →ₘ[volume] E) : V → E)) x
h₁ :
  HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((c • (↑(↑f : V →ₘ[volume] E) : V → E)) x) =
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊)
      (HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) ((↑(↑f : V →ₘ[volume] E) : V → E) x))
⊢ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑(c • f) : V →ₘ[volume] E) : V → E) x) =
    HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x))

Tactic:
rw [h, smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
c : ℂ
f : ↥(Lp E 1 volume)
x_1 x : V
h : (↑(↑(c • f) : V →ₘ[volume] E) : V → E) x = (c • (↑(↑f : V →ₘ[volume] E) : V → E)) x
⊢ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((c • (↑(↑f : V →ₘ[volume] E) : V → E)) x) =
    HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊)
      (HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) ((↑(↑f : V →ₘ[volume] E) : V → E) x))

Tactic:
simp
-- 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)
⊢ 0 ≤ ‖f‖

Tactic:
positivity
-- 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)
rw :
  ∀ (x : V),
    Norm.norm.{u_3} (E := E)
        (((({ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ : ↥(Lp E 1 volume) →ₗ[ℂ] V →ᵇ E } :
                    (a : ↥(Lp E 1 volume)) → V →ᵇ E)
                  f :
                V →ᵇ E) :
              (a : V) → E)
            x :
          E) ≤
      ‖f‖
⊢ Norm.norm (E := V →ᵇ E)
      (({ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ : ↥(Lp E 1 volume) →ₗ[ℂ] V →ᵇ E } :
            (a : ↥(Lp E 1 volume)) → V →ᵇ E)
          f :
        V →ᵇ E) ≤
    1 * ‖f‖

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

Premises used: BoundedContinuousFunction.norm_le, one_mul
-- 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‖
⊢ Norm.norm.{u_3} (E := E)
      (((({ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ : ↥(Lp E 1 volume) →ₗ[ℂ] V →ᵇ E } :
                  (a : ↥(Lp E 1 volume)) → V →ᵇ E)
                f :
              V →ᵇ E) :
            (a : V) → E)
          x :
        E) ≤
    ‖f‖

Tactic:
rw [LinearMap.coe_mk, AddHom.coe_mk, Lp.fourierTransform_apply, Real.fourier_eq]

Premises used: LinearMap.coe_mk, Real.Lp.fourierTransform_apply, Real.fourier_eq, AddHom.coe_mk
-- 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, ENNReal.toReal, Eq.symm, NNReal.toReal, 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)
⊢ (fourierTransformCLM V E : (a : ↥(Lp E 1 volume)) → V →ᵇ E) f = fourierTransform f

Tactic:
rfl

Premises used: BoundedContinuousFunction.ofNormedAddCommGroup, rfl, Real.Lp.fourierTransform
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x y : ℝ
rw : cexp ((↑(2 * π * y) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑1 : ℂ) * (↑y : ℂ) / (↑1 : ℂ))
⊢ Eq (α := ℂ) ((↑((𝐞 : (a : ℝ) → Circle) y) : ℂ) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
rw [fourierChar_apply, fourier_coe_apply]

Premises used: fourier_coe_apply, Real.fourierChar_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x y : ℝ
push_cast : cexp (2 * (↑π : ℂ) * (↑y : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * 1 * (↑y : ℂ) / 1)
⊢ cexp ((↑(2 * π * y) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑1 : ℂ) * (↑y : ℂ) / (↑1 : ℂ))

Tactic:
push_cast
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x y : ℝ
⊢ cexp (2 * (↑π : ℂ) * (↑y : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * 1 * (↑y : ℂ) / 1)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x : ℝ
⊢ ∀ (y : ℝ),
    Eq (α := ℂ) ((↑((𝐞 : (a : ℝ) → Circle) y) : ℂ) : ℂ)
      ((fourier 1 : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
have h1 (y : ℝ) : 𝐞 y = fourier 1 (y : UnitAddCircle) := by
    rw [fourierChar_apply, fourier_coe_apply]
    push_cast
    ring_nf
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x : ℝ
h1 :
  ∀ (y : ℝ),
    Eq (α := ℂ) ((↑((𝐞 : (a : ℝ) → Circle) y) : ℂ) : ℂ)
      ((fourier 1 : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasDerivAt (fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) (2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) x

Tactic:
simpa only [h1, Int.cast_one, ofReal_one, div_one, mul_one] using hasDerivAt_fourier 1 1 x

Premises used: Complex.ofReal_one, hasDerivAt_fourier, mul_one, OfNat.ofNat, div_one, Int.cast_one
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
⊢ Differentiable ℝ (F := ℂ) fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)

Tactic:
fun x ↦ (Real.hasDerivAt_fourierChar x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_fourierChar
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
x : ℝ
⊢ deriv (fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) x = 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)

Tactic:
(Real.hasDerivAt_fourierChar x).deriv

Premises used: HasDerivAt.deriv, Real.hasDerivAt_fourierChar
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w

Tactic:
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
⊢ HasFDerivAt
    ((fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) ∘
      (-fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w'))
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
      (ContinuousLinearMap.toSpanSingleton ℝ
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
      (-(L : (a : V) → W →L[ℝ] ℝ) v))
    w

Tactic:
(hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg

Premises used: HasFDerivAt.neg, HasFDerivAt.comp