-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem tsum_sq_fourierCoeff (f : Lp ℂ 2 <| @haarAddCircle T hT) :
    ∑' i : ℤ, ‖fourierCoeff f i‖ ^ 2 = ∫ t : AddCircle T, ‖f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = ∫ (x : AddCircle T), RCLike.re (inner (↑↑f x) (↑↑f x)) ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
simp only [← norm_sq_eq_inner] at H₃

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
⊢ ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2

Tactic:
simp

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = RCLike.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable (fun a => inner (↑↑f a) (↑↑f a)) haarAddCircle

Tactic:
exact L2.integrable_inner f f

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
have H₃ := congr_arg RCLike.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = RCLike.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ 0 < ENNReal.toReal 2

Tactic:
norm_num

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
have H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' i, ‖fourierBasis.repr f i‖ ^ 2 := by
  apply_mod_cast lp.norm_rpow_eq_tsum ?_ (fourierBasis.repr f)
  norm_num

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = RCLike.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
rw [← integral_re] at H₃

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = ∫ (x : AddCircle T), RCLike.re (inner (↑↑f x) (↑↑f x)) ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner f f) = RCLike.re (∫ (a : AddCircle T), inner (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable (fun a => inner (↑↑f a) (↑↑f a)) haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
simp_rw [← fourierBasis_repr]

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2

Tactic:
apply_mod_cast lp.norm_rpow_eq_tsum ?_ (fourierBasis.repr f)

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ 0 < ENNReal.toReal 2

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle

Tactic:
rw [← H₁, H₂, H₃]

Result:
no goals