awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
          ↥(Lp F 2 volume))
have h : norm (E := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
            (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
        f :
      ↥(Lp F 2 volume)) ≤
  norm (E := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
      ↥(Lp F 2 volume))
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ 𝓕⁻ (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕⁻ f).toLp 2 volume
have h_dense : DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
  (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
Tactic: apply LinearMap.extendOfNorm_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h_dense :
  DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
⊢ 𝓕⁻ (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕⁻ f).toLp 2 volume
have h_norm : ∃ (C : ℝ),
  ∀ (x : 𝓢(E, F)),
    norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
            x :
          ↥(Lp F 2 volume)) ≤
      C *
        norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
            ↥(Lp F 2 volume))
Tactic: apply LinearMap.extendOfNorm_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))
have h : ∀ (x : 𝓢(E, F)),
  norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          x :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
          ↥(Lp F 2 volume))
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
          ↥(Lp F 2 volume))
have h : norm (E := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
            (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
        f :
      ↥(Lp F 2 volume)) ≤
  norm (E := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
      ↥(Lp F 2 volume))
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))
have h : Eq (α := ↥(Lp F 2 volume))
  (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f : ↥(Lp F 2 volume))
  ((𝓕 (𝓕⁻ f)).toLp 2 volume : ↥(Lp F 2 volume))
Tactic: convert! (norm_fourier_toL2_eq (𝓕⁻ f)).symm.le
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
have hp : IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}
Tactic: apply DenseRange.induction_on (p := p)
    (SchwartzMap.denseRange_toLpCLM (p := 2) ENNReal.ofNat_ne_top) f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
hp : IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}
⊢ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
have ih : ∀ (a : 𝓢(E, F)), p ((toLpCLM ℝ F 2 volume : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) a)
Tactic: apply DenseRange.induction_on (p := p)
    (SchwartzMap.denseRange_toLpCLM (p := 2) ENNReal.ofNat_ne_top) f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}
have hp : Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution y)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
hp : Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution y)
⊢ IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}
have hp₁ : Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ toTemperedDistribution (𝓕 y)
Tactic: apply isClosed_eq
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution f) = 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f)))
have e_a : f = 𝓕 (𝓕⁻ f)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.LpSpace (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f))) = 𝓕⁻ (𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕⁻ f)))
have rw : 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f))) = 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f)))
Tactic: rw [fourier_toTemperedDistribution_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
Tactic: have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have simp_rw : Eq (α := ℝ)
  (⨆ (x : (↑(↑K : Set ℝ) : Type)),
    Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
  (⨆ (x : (↑(↑K : Set ℝ) : Type)),
    Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
Tactic: simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
simp_rw :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have simp_rw₁ : Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((e * g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
  (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
Tactic: simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
simp_rw :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((e * g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have simp_rw₂ : Eq (α := ℝ)
  (⨆ (x : (↑(↑K : Set ℝ) : Type)),
    ‖HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ)‖)
  (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
Tactic: simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
simp_rw :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((e * g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₂ :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      ‖HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ)‖)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have simp_rw₃ : Eq (α := ℝ)
  (⨆ (x : (↑(↑K : Set ℝ) : Type)),
    Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) * Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
  (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
Tactic: simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
simp_rw :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((e * g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₂ :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      ‖HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ)‖)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₃ :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) * Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
have simp_rw₄ : Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), 1 * Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
  (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
Tactic: simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
⊢ fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
  ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
Tactic: have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ := by
    have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
    intro K g
    simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
n : ℤ
⊢ e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
have h : ∀ (x : ℝ), Eq (α := ℂ) ((e.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
n : ℤ
x : ℝ
⊢ Eq (α := ℂ) ((e.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
have this : Periodic (α := ℝ) (β := ℂ) (⇑e : (a : ℝ) → ℂ) 1
Tactic: have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
⊢ fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑m : ℝ)
have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
Tactic: have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e := by
    intro n; ext1 x
    have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
    simpa only [mul_one] using this.int_mul n x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
⊢ fourierCoeff (T := 1)
      (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
      m =
    ∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
have simp_rw : HSMul.hSMul (β := ℂ) (1 / 1)
    (∫ (x : ℝ) in 0..HAdd.hAdd (α := ℝ) 0 1,
      HSMul.hSMul (α := ℂ) ((fourier (-m) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ))
          sorry (↑x : ℝ ⧸ AddSubgroup.zmultiples 1))) =
  ∫ (x : ℝ) in 0..1,
    HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ)
Tactic: simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]