awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
⊢ 𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) =
    HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
      (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) :
        𝓢(V, V →L[ℝ] E))
have h : ∀ (x m : V),
  Eq.{u_2 + 1} (α := E)
    ((((𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
    ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                  (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                      (𝓕 f) :
                    𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
Tactic: ext x m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x m : V
⊢ Eq.{u_2 + 1} (α := E)
    ((((𝓕 (E := 𝓢(V, V →L[ℝ] E)) ((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f : 𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
    ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                  (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                      (𝓕 f) :
                    𝓢(V, V →L[ℝ] E)) :
                (a : V) → V →L[ℝ] E)
              x :
            V →L[ℝ] E) :
          (a : V) → E)
        m :
      E)
have h : Eq.{u_2 + 1} (α := E) ((𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ (⇑f : (a : V) → E)) x : (a : V) → E) m : E)
  ((((HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (2 * (↑π : ℂ) * Complex.I)
                (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E))
                    (𝓕 f) :
                  𝓢(V, V →L[ℝ] E)) :
              (a : V) → V →L[ℝ] E)
            x :
          V →L[ℝ] E) :
        (a : V) → E)
      m :
    E)
Tactic: change 𝓕 (fderiv ℝ ⇑f) x m = _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ ∂_{m} (𝓕 f) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
have change : (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
    ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f)) =
  𝓕
    (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
Tactic: change SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E (𝓕 f)) = _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
      ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
have rw : 𝓕 (E := 𝓢(V, E))
    ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
        (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
          (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
            𝓢(V, V →L[ℝ] E))) :
      𝓢(V, E)) =
  𝓕
    (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
Tactic: rw [fderivCLM_fourier_eq, ← fourier_evalCLM_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕 (E := 𝓢(V, E))
      ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
          (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
            (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
              𝓢(V, V →L[ℝ] E))) :
        𝓢(V, E)) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E)))
have e_a : (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
    (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
        𝓢(V, V →L[ℝ] E))) =
  HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
    (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ (SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
      (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
          𝓢(V, V →L[ℝ] E))) =
    HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f : 𝓢(V, E))
have e_a : ∀ (x : V),
  Eq.{u_2 + 1} (α := E)
    ((((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
              (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
                (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                  𝓢(V, V →L[ℝ] E))) :
            𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
    ((HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
            (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m x : V
⊢ Eq.{u_2 + 1} (α := E)
    ((((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
              (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
                (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                  𝓢(V, V →L[ℝ] E))) :
            𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
    ((HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
            (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) f :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕 (∂_{m} f) =
    HSMul.hSMul (β := 𝓢(V, E)) (2 * (↑π : ℂ) * Complex.I)
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f) : 𝓢(V, E))
have change : 𝓕 (E := 𝓢(V, E))
    ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
        ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f) :
      𝓢(V, E)) =
  HSMul.hSMul (β := 𝓢(V, E)) (2 * (↑π : ℂ) * Complex.I)
    (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f) : 𝓢(V, E))
Tactic: change 𝓕 (SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E f)) = _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕 (E := 𝓢(V, E))
      ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
          ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f) :
        𝓢(V, E)) =
    HSMul.hSMul (β := 𝓢(V, E)) (2 * (↑π : ℂ) * Complex.I)
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f) : 𝓢(V, E))
have h : ∀ (x : V),
  Eq.{u_2 + 1} (α := E)
    ((𝓕 (E := 𝓢(V, E))
            ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
                ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f) :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
    ((HSMul.hSMul (β := 𝓢(V, E)) (2 * (↑π : ℂ) * Complex.I)
            (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f) :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m x : V
⊢ Eq.{u_2 + 1} (α := E)
    ((𝓕 (E := 𝓢(V, E))
            ((SchwartzMap.evalCLM ℝ V E m : (a : 𝓢(V, V →L[ℝ] E)) → 𝓢(V, E))
                ((fderivCLM ℝ V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f) :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
    ((HSMul.hSMul (β := 𝓢(V, E)) (2 * (↑π : ℂ) * Complex.I)
            (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕 f) :
              𝓢(V, E)) :
          (a : V) → E)
        x :
      E)
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕⁻ (∂_{m} f) =
    HSMul.hSMul (β := 𝓢(V, E)) (-(2 * (↑π : ℂ) * Complex.I))
      (((smulLeftCLM E fun (x : V) ↦ inner ℝ x m : 𝓢(V, E) →L[ℝ] 𝓢(V, E)) : (a : 𝓢(V, E)) → 𝓢(V, E)) (𝓕⁻ f) : 𝓢(V, E))
have this : Function.HasTemperateGrowth (F := ℝ) fun (x : V) ↦ inner ℝ x m
Tactic: have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕⁻ f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕⁻ g : (a : V) → F) x : F))
have h : ∀ (x : V), g = 𝓕 (𝓕⁻ g)
Tactic: convert! (integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℂ F
G : Type u_5
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace ℂ G
inst_11 : CompleteSpace E
inst_12 : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
h : ∀ (x : V), g = 𝓕 (𝓕⁻ g)
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((𝓕⁻ f : (a : V) → E) ξ) : F →L[ℂ] G) : (a : F) → G) ((g : (a : V) → F) ξ : F))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      (((M : (a : E) → F →L[ℂ] G) ((f : (a : V) → E) x) : F →L[ℂ] G) : (a : F) → G) ((𝓕⁻ g : (a : V) → F) x : F))
have h₁ : ∀ (x : V), f = 𝓕 (𝓕⁻ f)
Tactic: convert! (integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
x : V
⊢ Norm.norm.{u_4} (E := F) ((𝓕 f : (a : V) → F) x : F) =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
have rw : ‖𝓕 (E := (a : V) → F) (⇑f : (a : V) → F) x‖ =
  Norm.norm.{u_4} (E := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
Tactic: rw [fourier_coe, Real.fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
x : V
rw :
  ‖𝓕 (E := (a : V) → F) (⇑f : (a : V) → F) x‖ =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
⊢ Norm.norm.{u_4} (E := F) ((𝓕 f : (a : V) → F) x : F) =
    Norm.norm.{u_4} (E := F)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
have rw₁ : Norm.norm.{u_4} (E := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F)) =
  Norm.norm.{u_4} (E := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) (β := F) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ v x) : Circle) ((f : (a : V) → F) v : F))
Tactic: rw [fourier_coe, Real.fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ‖(𝓕 f).toBoundedContinuousFunction‖ ≤ Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)
have rw : ∀ (x : V),
  Norm.norm.{u_4} (E := F) (((𝓕 f).toBoundedContinuousFunction : (a : V) → F) x : F) ≤
    Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)
Tactic: rw [BoundedContinuousFunction.norm_le (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f : 𝓢(V, H)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((𝓕 f : (a : V) → H) ξ : H)) 2)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((f : (a : V) → H) x : H)) 2)
have a : Eq (α := ℂ)
  ((Complex.ofRealLI : (a : ℝ) → ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
        HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((𝓕 f : (a : V) → H) ξ : H)) 2) :
    ℂ)
  ((Complex.ofRealLI : (a : ℝ) → ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
        HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((f : (a : V) → H) x : H)) 2) :
    ℂ)
Tactic: apply Complex.ofRealLI.injective
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f : 𝓢(V, H)
⊢ Norm.norm (E := ↥(Lp H 2 volume)) ((𝓕 f).toLp 2 volume) = Norm.norm (E := ↥(Lp H 2 volume)) (f.toLp 2 volume)
have simp_rw : √((RCLike.re : (a : ℂ) → ℝ) (inner ℂ (E := ↥(Lp H 2 volume)) ((𝓕 f).toLp 2 volume) ((𝓕 f).toLp 2 volume))) =
  √((RCLike.re : (a : ℂ) → ℝ) (inner ℂ (E := ↥(Lp H 2 volume)) (f.toLp 2 volume) (f.toLp 2 volume)))
Tactic: simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourier_toL2_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (besselPotential E F 0) (ContinuousLinearMap.id ℂ 𝓢'(E, F))
have h : ∀ (f : 𝓢'(E, F)) (x : 𝓢(E, ℂ)),
  Eq.{u_2 + 1} (α := F) ((((besselPotential E F 0 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
    ((((ContinuousLinearMap.id ℂ 𝓢'(E, F) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f) :
      𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
have rw : Eq (α := 𝓢'(E, F))
  ((fourierMultiplierCLM F
          (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
            (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) :
        (a : 𝓢'(E, F)) → 𝓢'(E, F))
      f :
    𝓢'(E, F))
  ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
        (a : 𝓢'(E, F)) → 𝓢'(E, F))
      f :
    𝓢'(E, F))
Tactic: rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
have e_a : (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
    (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) =
  fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) =
    fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
have e_a : ∀ (x : E),
  HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
      (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) x =
    (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) * (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ) =
    (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
have e_a : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
Tactic: norm_cast