awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
have 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)
Tactic: filter_upwards [Lp.coeFn_add f g] with x h₁
-- 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_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 + 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)
have 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)
Tactic: rw [h₁]
-- 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
⊢ @Integrable.{u_3, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) v)) volume
have h : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑f : V →ₘ[volume] E) : V → E) volume
Tactic: rw [Real.fourierIntegral_convergent_iff]
-- 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
⊢ @Integrable.{u_3, u_1} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪v, x⟫) : 𝕊) ((↑(↑g : V →ₘ[volume] E) : V → E) v)) volume
have h : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (↑(↑g : V →ₘ[volume] E) : V → E) volume
Tactic: rw [Real.fourierIntegral_convergent_iff]
-- 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
c : ℂ
f : ↥(Lp E 1 volume)
⊢ fourierTransform (c • f) = HSMul.hSMul (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ) (fourierTransform f)
have 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)
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
c : ℂ
f : ↥(Lp E 1 volume)
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)
have 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))
Tactic: simp only [Lp.fourierTransform_apply, BoundedContinuousFunction.coe_smul, 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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
⊢ (@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))
have 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)))
Tactic: rw [← integral_smul]
-- 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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
⊢ 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)))
have 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))
Tactic: apply integral_congr_ae
-- 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
c : ℂ
f : ↥(Lp E 1 volume)
x : V
⊢ 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))
have 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))
Tactic: filter_upwards [Lp.coeFn_smul c f] with x h
-- 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
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 (α := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      (HSMul.hSMul (α := 𝕊) ((𝐞 : (a : ℝ) → 𝕊) (-⟪x, x_1⟫) : 𝕊) ((↑(↑f : V →ₘ[volume] E) : V → E) x))
have 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))
Tactic: rw [h, smul_comm]
-- 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)
⊢ 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‖
have rw : ∀ (x : V),
  Norm.norm.{u_3} (E := E)
      (((({ toFun := fourierTransform, map_add' := sorry, map_smul' := sorry : ↥(Lp E 1 volume) →ₗ[ℂ] V →ᵇ E } :
                  (a : ↥(Lp E 1 volume)) → V →ᵇ E)
                f :
              V →ᵇ E) :
            (a : V) → E)
          x :
        E) ≤
    ‖f‖
Tactic: rw [one_mul, BoundedContinuousFunction.norm_le (by positivity)]
-- 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)
      (((({ 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‖
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 [LinearMap.coe_mk, AddHom.coe_mk, Lp.fourierTransform_apply, Real.fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
x y : ℝ
⊢ Eq (α := ℂ) ((↑((𝐞 : (a : ℝ) → Circle) y) : ℂ) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have rw : cexp ((↑(2 * π * y) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑1 : ℂ) * (↑y : ℂ) / (↑1 : ℂ))
Tactic: rw [fourierChar_apply, fourier_coe_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
x y : ℝ
⊢ cexp ((↑(2 * π * y) : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * (↑1 : ℂ) * (↑y : ℂ) / (↑1 : ℂ))
have push_cast : cexp (2 * (↑π : ℂ) * (↑y : ℂ) * I) = cexp (2 * (↑π : ℂ) * I * 1 * (↑y : ℂ) / 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
Goal:
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) (2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) x
have h1 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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
    (fun (w : W) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
    (HSMul.hSMul (β := W →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)))
    w
have ha : 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)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 (w : W) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
    (HSMul.hSMul (β := W →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)))
    w
have h : addCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule →
    HSMul.hSMul (β := W →L[ℝ] ℂ)
        (-2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
        (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) =
      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)
Tactic: convert! (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
e_8 : addCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
⊢ HSMul.hSMul (β := W →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) =
    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)
have h : ∀ (y : W),
  Eq (α := ℂ)
    ((HSMul.hSMul (β := W →L[ℝ] ℂ)
            (-2 * (↑π : ℂ) * I *
              (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
            (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) :
          (a : W) → ℂ)
        y :
      ℂ)
    ((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) :
          (a : W) → ℂ)
        y :
      ℂ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
e_8 : addCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
y : W
⊢ Eq (α := ℂ)
    ((HSMul.hSMul (β := W →L[ℝ] ℂ)
            (-2 * (↑π : ℂ) * I *
              (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
            (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) :
          (a : W) → ℂ)
        y :
      ℂ)
    ((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) :
          (a : W) → ℂ)
        y :
      ℂ)
have h : 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
    (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
  (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
    (2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
Tactic: simp only [neg_mul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
    ContinuousLinearMap.neg_apply, ContinuousLinearMap.toSpanSingleton_apply, real_smul, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 y : W
⊢ (fderiv ℝ
          (fun (w : W) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
          w :
        (a : W) → ℂ)
      y =
    -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
have simp : 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
    (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
  2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
    (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
Tactic: simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul,
    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 y : V
w : W
⊢ (fderiv ℝ
          (fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
          v :
        (a : V) → ℂ)
      y =
    -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
have simp : 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
    (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) =
  2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) *
    (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
Tactic: simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul,
    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]