awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i‖ 2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have simp_rw : HasSum (α := ℝ)
  (fun (i : ℤ) ↦
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i))
      2)
  (∫ (t : AddCircle T),
    HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
Tactic: simp_rw [← fourierBasis_repr]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
have apply_mod_cast : 0 < ENNReal.toReal 2
Tactic: apply_mod_cast lp.hasSum_norm ?_ (fourierBasis.repr f)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have H₁ : HasSum
  (fun (i : ℤ) ↦
    HPow.hPow (β := ℕ)
      (norm (E := (fun (x : ℤ) ↦ ℂ) i)
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
          i))
      2)
  (HPow.hPow (β := ℕ)
    (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
      ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
        ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
    2)
Tactic: have H₁ : HasSum (fun i => ‖fourierBasis.repr f i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2) := by
    apply_mod_cast lp.hasSum_norm ?_ (fourierBasis.repr f)
    simp
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have H₂ : HPow.hPow (β := ℕ)
    (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
      ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
        ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
    2 =
  HPow.hPow (β := ℕ) ‖f‖ 2
Tactic: have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have H₃ : Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
  ((RCLike.re : (a : ℂ) → ℝ)
      (∫ (a : AddCircle T),
        inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
          ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle) :
    ℝ)
Tactic: have H₃ := congr_arg RCLike.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
H₃ :
  Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
    ((RCLike.re : (a : ℂ) → ℝ)
        (∫ (a : AddCircle T),
          inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
            ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle) :
      ℝ)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have rw : ∀
  (H₃ :
    Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
      (∫ (x : AddCircle T),
          (RCLike.re : (a : ℂ) → ℝ)
            (inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)
              ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)) ∂haarAddCircle :
        ℝ)),
  HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
Tactic: rw [← integral_re] at H₃
Cleared hypotheses: H₃
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
H₃ :
  Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
    ((RCLike.re : (a : ℂ) → ℝ)
        (∫ (a : AddCircle T),
          inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
            ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle) :
      ℝ)
rw :
  ∀
    (H₃ :
      Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
        (∫ (x : AddCircle T),
            (RCLike.re : (a : ℂ) → ℝ)
              (inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)
                ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)) ∂haarAddCircle :
          ℝ)),
    HasSum (α := ℝ)
      (fun (i : ℤ) ↦
        HPow.hPow (β := ℕ)
          (norm (E := ℂ)
            ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
                (i : ℤ) → ℂ)
              i))
          2)
      (∫ (t : AddCircle T),
        HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have rw₁ : Integrable (ε := ℂ)
  (fun (a : AddCircle T) ↦
    inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
  haarAddCircle
Tactic: rw [← integral_re] at H₃
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
H₃ :
  Eq (α := ℝ) ((RCLike.re : (a : ℂ) → ℝ) (inner ℂ f f) : ℝ)
    (∫ (x : AddCircle T),
        (RCLike.re : (a : ℂ) → ℝ)
          (inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)
            ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x)) ∂haarAddCircle :
      ℝ)
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have H₄ : HPow.hPow (β := ℕ) ‖f‖ 2 =
  ∫ (x : AddCircle T),
    HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle
Tactic: simp only [← norm_sq_eq_re_inner] at H₃
Cleared hypotheses: H₃
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ :
  HasSum
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := (fun (x : ℤ) ↦ ℂ) i)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
            i))
        2)
    (HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2)
H₂ :
  HPow.hPow (β := ℕ)
      (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
        ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
          ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
      2 =
    HPow.hPow (β := ℕ) ‖f‖ 2
H₃ :
  HPow.hPow (β := ℕ) ‖f‖ 2 =
    ∫ (x : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle
⊢ HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
have rwa : ∀
  (H₁ :
    HasSum
      (fun (i : ℤ) ↦
        HPow.hPow (β := ℕ)
          (norm (E := (fun (x : ℤ) ↦ ℂ) i)
            ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
                (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
              i))
          2)
      (HPow.hPow (β := ℕ) ‖f‖ 2))
  (H₂ :
    HPow.hPow (β := ℕ)
        (norm (E := ↥(lp (fun (x : ℤ) ↦ ℂ) 2))
          ((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f :
            ↥(lp (fun (x : ℤ) ↦ ℂ) 2)))
        2 =
      HPow.hPow (β := ℕ) ‖f‖ 2)
  (H₃ :
    HPow.hPow (β := ℕ) ‖f‖ 2 =
      ∫ (x : AddCircle T),
        HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) x‖ 2 ∂haarAddCircle),
  HasSum (α := ℝ)
    (fun (i : ℤ) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
              (i : ℤ) → ℂ)
            i))
        2)
    (∫ (t : AddCircle T),
      HPow.hPow (β := ℕ) ‖(↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t‖ 2 ∂haarAddCircle)
Tactic: rwa [H₂, H₃] at H₁
Cleared hypotheses: H₁, H₂, H₃
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
⊢ 0 < b - a
have linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))
have this : Fact (0 < b - a)
Tactic: haveI := Fact.mk (by linarith : 0 < b - a)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
this : Fact (0 < b - a)
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))
have hL2₁ : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
Tactic: rw [← add_sub_cancel a b] at hL2
Cleared hypotheses: hL2, this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (hypothesis)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))
have h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
Tactic: have h := hL2.memLp_liftIoc.haarAddCircle
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))
have h₁ : Eq (α := ℤ → ℝ) (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2) fun (i : ℤ) ↦
  HPow.hPow (β := ℕ)
    ‖fourierCoeff
        (↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) i‖
    2
Tactic: convert! hasSum_sq_fourierCoeff h.toLp using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
h₁ :
  Eq (α := ℤ → ℝ) (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2) fun (i : ℤ) ↦
    HPow.hPow (β := ℕ)
      ‖fourierCoeff
          (↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) i‖
      2
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))
have h₂ : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2) =
  ∫ (t : AddCircle (b - a)),
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
      2 ∂haarAddCircle
Tactic: convert! hasSum_sq_fourierCoeff h.toLp using 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2) =
    ∫ (t : AddCircle (b - a)),
      HPow.hPow (β := ℕ)
        ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
        2 ∂haarAddCircle
have h₁ : HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..a + (b - a), HPow.hPow (β := ℕ) ‖f x‖ 2) =
  ∫ (t : AddCircle (b - a)),
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
      2 ∂haarAddCircle
Tactic: nth_rw 2 [← add_sub_cancel a b]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..a + (b - a), HPow.hPow (β := ℕ) ‖f x‖ 2) =
    ∫ (t : AddCircle (b - a)),
      HPow.hPow (β := ℕ)
        ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
        2 ∂haarAddCircle
have h₁ : HSMul.hSMul (β := ℝ) (b - a)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a_1 : AddCircle (b - a)) ↦
      liftIoc (b - a) a ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ∘ f) a_1) =
  ∫ (t : AddCircle (b - a)),
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
      2 ∂haarAddCircle
Tactic: rw [← AddCircle.integral_liftIoc_eq_intervalIntegral, ← Function.comp_def (f := (‖·‖ ^ 2))]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ HSMul.hSMul (β := ℝ) (b - a)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a_1 : AddCircle (b - a)) ↦
        liftIoc (b - a) a ((fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ∘ f) a_1) =
    ∫ (t : AddCircle (b - a)),
      HPow.hPow (β := ℕ)
        ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
        2 ∂haarAddCircle
have h₁ : Eq (α := ℝ) (∫ (t : AddCircle (b - a)), HPow.hPow (β := ℕ) ‖liftIoc (b - a) a f t‖ 2 ∂haarAddCircle)
  (∫ (t : AddCircle (b - a)),
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
      2 ∂haarAddCircle)
Tactic: simp only [liftIoc_comp_apply, ← AddCircle.integral_haarAddCircle]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ Eq (α := ℝ) (∫ (t : AddCircle (b - a)), HPow.hPow (β := ℕ) ‖liftIoc (b - a) a f t‖ 2 ∂haarAddCircle)
    (∫ (t : AddCircle (b - a)),
      HPow.hPow (β := ℕ)
        ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) t‖
        2 ∂haarAddCircle)
have h₁ : (ae (F := Measure (AddCircle (b - a))) haarAddCircle).EventuallyEq (β := ℝ)
  (fun (a_1 : AddCircle (b - a)) ↦ HPow.hPow (β := ℕ) ‖liftIoc (b - a) a f a_1‖ 2) fun (a_1 : AddCircle (b - a)) ↦
  HPow.hPow (β := ℕ)
    ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) a_1‖ 2
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircle (goal)
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (ae (F := Measure (AddCircle (b - a))) haarAddCircle).EventuallyEq (β := ℝ)
    (fun (a_1 : AddCircle (b - a)) ↦ HPow.hPow (β := ℕ) ‖liftIoc (b - a) a f a_1‖ 2) fun (a_1 : AddCircle (b - a)) ↦
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) a_1‖ 2
have h₁ : ∀ (x : AddCircle (b - a))
  (hx :
    (↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) x =
      liftIoc (b - a) a f x),
  HPow.hPow (β := ℕ) ‖liftIoc (b - a) a f x‖ 2 =
    HPow.hPow (β := ℕ)
      ‖(↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ) x‖ 2
Tactic: filter_upwards [h.coeFn_toLp] with x hx