theorem FourierFacts.fourier_sine_theorem (f : ℝ → ℝ) (hf : MeasureTheory.Integrable (fun (x : ℝ) => f x ^ 2) (MeasureTheory.volume.restrict (Set.Icc 0 1))) : Filter.Tendsto (fun (N : ℕ) => HeatEquation.L2ErrorSq f N) Filter.atTop (nhds 0) ∧ HeatEquation.L2NormSq f = ∑' (m : ℕ), 1 / 2 * HeatEquation.fourierSineCoeff f (m + 1) ^ 2 ∧ (ContinuousOn f (Set.Icc 0 1) → ∀ (a b : ℝ), 0 < a → a ≤ b → b < 1 → Filter.Tendsto (fun (N : ℕ) => ⨆ x ∈ Set.Icc a b, |f x - HeatEquation.fourierSinePartialSum f N x|) Filter.atTop (nhds 0))

Basic facts about the Fourier sine series on $[0, 1]$ (Theorem 4.1): for $f \in L^2([0, 1])$, the Fourier sine partial sums converge to $f$ in $L^2$, the Parseval identity $\|f\|_{L^2}^2 = \sum_m \tfrac{1}{2} A_m^2$ holds, and if $f$ is continuous on $[0, 1]$ then the convergence is uniform on any closed subinterval $[a, b] \subset (0, 1)$.

theorem FourierFacts.fourier_sine_uniform_convergence (f : ℝ → ℝ) (hf_cont : ContinuousOn f (Set.Icc 0 1)) (a b : ℝ) (hab : 0 < a) (hba : a ≤ b) (hb1 : b < 1) : Filter.Tendsto (fun (N : ℕ) => ⨆ x ∈ Set.Icc a b, |f x - HeatEquation.fourierSinePartialSum f N x|) Filter.atTop (nhds 0)

Uniform convergence statement from Theorem 4.1: if $f$ is continuous on $[0, 1]$, then the Fourier sine partial sums converge uniformly to $f$ on any closed subinterval $[a, b] \subset (0, 1)$.