awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f t))

Tactic:
setIntegral_congr_fun measurableSet_Ioo fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioo
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
e_a :
  ∀ (x : ℝ) (hx : x ∈ Ioo a (a + T)),
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
        (liftIco T a f (↑t : ℝ ⧸ AddSubgroup.zmultiples T)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioo a (a + T))) fun (t : ℝ) ↦
      HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑t : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f t))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioo fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioo
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ioo a (a + T)
e_a e_a₁ :
  HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)
⊢ HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ)
      (liftIco T a f (↑x : ℝ ⧸ AddSubgroup.zmultiples T)) =
    HSMul.hSMul (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ) (f x)

Tactic:
rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]

Premises used: Set.Ioo_subset_Ico_self, AddCircle.liftIco_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ Eq (α := (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) (⇑fourierBasis : (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2)

Tactic:
HilbertBasis.coe_mk _ _

Premises used: HilbertBasis.coe_mk, Set.Mem, setOf
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
trans :
  Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
trans₁ :
  ∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i
⊢ (↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i

Tactic:
trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle

Premises used: AddCircle, AddCircle.haarAddCircle
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
rw :
  Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    (∫ (a : AddCircle T),
      inner ℂ ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)
⊢ Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
        (i : ℤ) → (fun (x : ℤ) ↦ ℂ) i)
      i)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)

Tactic:
rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]

Premises used: MeasureTheory.L2.inner_def, fourierBasis, coe_fourierBasis, HilbertBasis.repr_apply_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ Eq (α := (fun (x : ℤ) ↦ ℂ) i)
    (∫ (a : AddCircle T),
      inner ℂ ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) ∂haarAddCircle)
    (∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle)

Tactic:
simp only [RCLike.inner_apply']

Premises used: RCLike.inner_apply'
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
h :
  (ae (F := Measure (AddCircle T)) haarAddCircle).EventuallyEq (β := (fun (x : ℤ) ↦ ℂ) i)
    (fun (a : AddCircle T) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
    fun (a : AddCircle T) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
⊢ ∫ (t : AddCircle T),
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) t) ∂haarAddCircle =
    fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
h :
  ∀ (a : AddCircle T)
    (ht :
      (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a =
        (fourier i : (a : AddCircle T) → ℂ) a),
    HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
      HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
⊢ (ae (F := Measure (AddCircle T)) haarAddCircle).EventuallyEq (β := (fun (x : ℤ) ↦ ℂ) i)
    (fun (a : AddCircle T) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) :
          ℂ)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
    fun (a : AddCircle T) ↦
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)

Tactic:
filter_upwards [coeFn_fourierLp 2 i] with _ ht

Premises used: OfNat.ofNat, coeFn_fourierLp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a : AddCircle T
ht : (↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a = (fourier i : (a : AddCircle T) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((fourier i : (a : AddCircle T) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
h₁ :
  HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
h₂ h₃ :
  HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HMul.hMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(fourierLp 2 i) : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((fourier (-i) : (a : AddCircle T) → ℂ) a : ℂ)
      ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)

Tactic:
rw [ht, ← fourier_neg, smul_eq_mul]

Premises used: fourier_neg, smul_eq_mul
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
simp_rw :
  HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        (fourierLp 2 i))
    f
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ↥(Lp ℂ 2 haarAddCircle))
        (fourierCoeff (↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) i) (fourierLp 2 i))
    f

Tactic:
simp_rw [← fourierBasis_repr]

Premises used: fourierBasis_repr
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
rw :
  HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        ((fourierBasis : (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) i : ↥(Lp ℂ 2 haarAddCircle)))
    f
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        (fourierLp 2 i))
    f

Tactic:
rw [← coe_fourierBasis]

Premises used: coe_fourierBasis
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        ((fourierBasis : (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) i : ↥(Lp ℂ 2 haarAddCircle)))
    f

Tactic:
HilbertBasis.hasSum_repr fourierBasis f

Premises used: Set.Mem, setOf, HilbertBasis.hasSum_repr, fourierBasis
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        ((↑((HilbertBasis.repr fourierBasis : (a : ↥(Lp ℂ 2 haarAddCircle)) → ↥(lp (fun (x : ℤ) ↦ ℂ) 2)) f) :
            (i : ℤ) → ℂ)
          i)
        ((fourierBasis : (a : ℤ) → ↥(Lp ℂ 2 haarAddCircle)) i : ↥(Lp ℂ 2 haarAddCircle)))
    f

Tactic:
exact HilbertBasis.hasSum_repr fourierBasis f

Premises used: HilbertBasis.hasSum_repr, fourierBasis
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
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)
⊢ 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)

Tactic:
simp_rw [← fourierBasis_repr]

Premises used: fourierBasis_repr
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
apply_mod_cast : 0 < ENNReal.toReal 2
⊢ 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:
apply_mod_cast lp.hasSum_norm ?_ (fourierBasis.repr f)

Premises used: HilbertBasis.repr, fourierBasis, lp.hasSum_norm, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ 0 < ENNReal.toReal 2

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)

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
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ 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:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ 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
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
⊢ 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)
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
rw₁ :
  Integrable (ε := ℂ)
    (fun (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)

Tactic:
rw [← integral_re] at H₃

Premises used: integral_re
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 :
      ℝ)
⊢ 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₃

Premises used: InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.Fourier.AddCircle
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) :
      ℝ)
⊢ Integrable (ε := ℂ)
    (fun (a : AddCircle T) ↦
      inner ℂ ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a)
        ((↑(↑f : AddCircle T →ₘ[haarAddCircle] ℂ) : AddCircle T → ℂ) a))
    haarAddCircle

Tactic:
L2.integrable_inner f f

Premises used: MeasureTheory.L2.integrable_inner