awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact L2.integrable_inner f f

Premises used: MeasureTheory.L2.integrable_inner
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ Eq (α := ℝ)
    (∑' (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:
(hasSum_sq_fourierCoeff _).tsum_eq

Premises used: HasSum.tsum_eq, hasSum_sq_fourierCoeff
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
linarith : b - a ≤ 0 → a - b + (b - a - 0) = 0
⊢ 0 < b - a

Tactic:
linarith
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
⊢ Fact (0 < b - a)

Tactic:
haveI := Fact.mk (by linarith : 0 < b - a)
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))

Tactic:
rw [← add_sub_cancel a b] at hL2

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
hL2₁ : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a (a + (b - a))))
⊢ Fact (0 < b - a)

Tactic:
rw [← add_sub_cancel a b] at hL2

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Fourier.AddCircle
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)
⊢ MemLp (liftIoc (b - a) a f) 2 haarAddCircle

Tactic:
have h := hL2.memLp_liftIoc.haarAddCircle
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (β := ℕ)
        ‖fourierCoeff
            (↑(↑(MemLp.toLp (liftIoc (b - a) a f) h) : AddCircle (b - a) →ₘ[haarAddCircle] ℂ) : AddCircle (b - a) → ℂ)
            i‖
        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:
hasSum_sq_fourierCoeff h.toLp

Premises used: MeasureTheory.MemLp.toLp, hasSum_sq_fourierCoeff
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
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
⊢ HasSum (fun (i : ℤ) ↦ HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2)
    (HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2))

Tactic:
convert! hasSum_sq_fourierCoeff h.toLp using 1

Premises used: MeasureTheory.MemLp.toLp, hasSum_sq_fourierCoeff
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (α := ℤ → ℝ) (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:
simp [fourierCoeff_congr_ae h.coeFn_toLp, fourierCoeff_liftIoc_eq]

Premises used: MeasureTheory.MemLp.coeFn_toLp, fourierCoeff_congr_ae, fourierCoeff_liftIoc_eq
-- Module: Mathlib.Analysis.Fourier.AddCircle
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₁ :
  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
⊢ 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:
nth_rw 2 [← add_sub_cancel a b]

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Fourier.AddCircle
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₁ :
  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
⊢ 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:
rw [← AddCircle.integral_liftIoc_eq_intervalIntegral, ← Function.comp_def (f := (‖·‖ ^ 2))]

Premises used: Norm.norm, Function.comp_def, HPow.hPow, AddCircle.integral_liftIoc_eq_intervalIntegral, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.AddCircle
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 (α := ℝ) (∫ (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)
⊢ 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:
simp only [liftIoc_comp_apply, ← AddCircle.integral_haarAddCircle]

Premises used: AddCircle.integral_haarAddCircle, AddCircle.liftIoc_comp_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
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₁ :
  (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
⊢ 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:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.AddCircle
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₁ :
  ∀ (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
⊢ (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:
filter_upwards [h.coeFn_toLp] with x hx

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircle
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
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:
simp [hx]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp (m0 := MeasureSpace.toMeasurableSpace) f 2 (Measure.restrict volume (Ioc a b))
⊢ ∑' (i : ℤ), HPow.hPow (β := ℕ) ‖fourierCoeffOn hab f i‖ 2 =
    HSMul.hSMul (β := ℝ) (b - a)⁻¹ (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ‖f x‖ 2)

Tactic:
(hasSum_sq_fourierCoeffOn _ hL2).tsum_eq

Premises used: hasSum_sq_fourierCoeffOn, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
n : ℤ
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ :
  ∀ (x : AddCircle T),
    Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)
⊢ ∀ (x : AddCircle T),
    Eq (α := ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ) ((fourier (-n) : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
tauto
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
⊢ HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        (fourierCoeff (T := T)
          (↑(↑((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f) :
                AddCircle T →ₘ[haarAddCircle] ℂ) :
            AddCircle T → ℂ)
          i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))

Tactic:
have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle))
        (fourierCoeff (T := T)
          (↑(↑((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f) :
                AddCircle T →ₘ[haarAddCircle] ℂ) :
            AddCircle T → ℂ)
          i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))

Tactic:
simp_rw [fourierCoeff_toLp] at sum_L2

Premises used: fourierCoeff_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ HasSum
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i) (fourier i))
    f

Tactic:
ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2

Premises used: Summable.of_norm, ContinuousMap.hasSum_of_hasSum_Lp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
simp_rw : Summable (α := ℝ) fun (a : ℤ) ↦ norm (E := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a)
⊢ Summable (α := ℝ) fun (a : ℤ) ↦
    ‖HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a) (fourier a)‖

Tactic:
simp_rw [norm_smul, fourier_norm, mul_one]

Premises used: norm_smul, fourier_norm, mul_one
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ Summable (α := ℝ) fun (a : ℤ) ↦ norm (E := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a)

Tactic:
h.norm

Premises used: Summable.norm
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 haarAddCircle))
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 haarAddCircle)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        (fourierLp 2 i))
    ((toLp 2 haarAddCircle ℂ : (a : C(AddCircle T, ℂ)) → ↥(Lp ℂ 2 haarAddCircle)) f : ↥(Lp ℂ 2 haarAddCircle))
⊢ Summable (α := ℝ) fun (a : ℤ) ↦ norm (E := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) a)

Tactic:
exact h.norm

Premises used: Summable.norm
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
x : AddCircle T
⊢ HasSum (α := ℂ)
    (fun (b : ℤ) ↦
      ((evalCLM ℂ x : (a : C(AddCircle T, ℂ)) → ℂ)
          (HSMul.hSMul (α := ℂ) (β := C(AddCircle T, ℂ)) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) b)
            (fourier b)) :
        ℂ))
    ((evalCLM ℂ x : (a : C(AddCircle T, ℂ)) → ℂ) f : ℂ)

Tactic:
(ContinuousMap.evalCLM ℂ x).hasSum (hasSum_fourier_series_of_summable h)

Premises used: ContinuousLinearMap.hasSum, ContinuousMap.evalCLM, hasSum_fourier_series_of_summable, Complex
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (α := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ))
x : AddCircle T
⊢ HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := T) (⇑f : (a : AddCircle T) → ℂ) i)
        ((fourier i : (a : AddCircle T) → ℂ) x : ℂ))
    ((f : (a : AddCircle T) → ℂ) x : ℂ)

Tactic:
convert! (ContinuousMap.evalCLM ℂ x).hasSum (hasSum_fourier_series_of_summable h)

Premises used: ContinuousLinearMap.hasSum, ContinuousMap.evalCLM, hasSum_fourier_series_of_summable, Complex
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
h :
  ∀ (m : ℤ),
    Eq (α := ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ) m : ℂ)
      (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)
⊢ Eq (α := (n : ℤ) → ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ))
    (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1)

Tactic:
ext m
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
h : inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
⊢ Eq (α := ℂ) (fourierCoeff (T := T) (⇑(fourier n) : (a : AddCircle T) → ℂ) m : ℂ)
    (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)

Tactic:
rw [← fourierCoeff_congr_ae (coeFn_fourierLp 2 n), ← fourierBasis_repr,
    HilbertBasis.repr_apply_apply, coe_fourierBasis]

Premises used: coe_fourierBasis, HilbertBasis.repr_apply_apply, fourierBasis_repr, fourierCoeff_congr_ae, OfNat.ofNat, coeFn_fourierLp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
h : inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 m) = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
h₁ :
  ∀ (hmn : m ≠ n),
    inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m

Tactic:
obtain (rfl | hmn) := eq_or_ne m n

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
m : ℤ
h : HPow.hPow (α := ℂ) (β := ℕ) (↑1 : ℂ) 2 = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 m) = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m

Tactic:
rw [inner_self_eq_norm_sq_to_K, (orthonormal_fourier (hT := hT)).1 m]

Premises used: inner_self_eq_norm_sq_to_K, orthonormal_fourier, And.left
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ HPow.hPow (α := ℂ) (β := ℕ) (↑1 : ℂ) 2 = Pi.single (M := fun (j : ℤ) ↦ ℂ) m 1 m

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
h : Eq (α := ℂ) (0 : ℂ) (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)
⊢ inner ℂ (E := ↥(Lp ℂ 2 haarAddCircle)) (fourierLp 2 m) (fourierLp 2 n) = Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m

Tactic:
rw [(orthonormal_fourier (hT := hT)).2 hmn]

Premises used: orthonormal_fourier, And.right
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ Eq (α := ℂ) (0 : ℂ) (Pi.single (M := fun (j : ℤ) ↦ ℂ) n 1 m : ℂ)

Tactic:
simp [hmn]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
simp_rw :
  HasDerivAt (fun (y : ℝ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑y : ℂ) / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (fourier n : (a : AddCircle T) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples T))
    (HMul.hMul (β := ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))
      ((fourier n : (a : AddCircle T) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) : ℂ))
    x

Tactic:
simp_rw [fourier_coe_apply]

Premises used: fourier_coe_apply
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑y : ℂ) / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) x

Tactic:
(?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal

Premises used: HasDerivAt.comp_ofReal
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
refine :
  HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑y : ℂ) / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) x

Tactic:
refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal

Premises used: HasDerivAt.comp_ofReal
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
α β : ℂ
⊢ α * cexp β = cexp β * α

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
rw :
  HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)) * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ))) (↑x : ℂ)

Tactic:
rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]
-- Module: Mathlib.Analysis.Fourier.AddCircle
Goal:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun (y : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * y / (↑T : ℂ)))
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) / (↑T : ℂ)) * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑T : ℂ))) (↑x : ℂ)

Tactic:
(hasDerivAt_exp _).comp (x : ℂ) ?_

Premises used: HasDerivAt.comp, Complex.ofReal, Complex.hasDerivAt_exp