structure HeatEquation.DirichletHeatProblem1D : Type

Data for the 1-dimensional Dirichlet problem for the heat equation on a rod of length $L$ over the time interval $[0, T]$: diffusion constant $D > 0$, internal forcing $f(t, x)$, initial profile $g(x)$, and boundary data $h_0(t), h_L(t)$ at $x = 0$ and $x = L$ respectively.

• L : ℝ
• T : ℝ
• D : ℝ
• g : ℝ → ℝ
• h₀ : ℝ → ℝ
• hL : ℝ → ℝ
• f : ℝ → ℝ → ℝ
• hL_pos : self.L > 0
• hT_pos : self.T > 0
• hD_pos : self.D > 0

noncomputable def HeatEquation.fourierSineCoeff (f : ℝ → ℝ) (m : ℕ) : ℝ

The $m$-th Fourier sine coefficient of $f$ on $[0, 1]$: $A_m = 2 \int_0^1 f(x) \sin(m \pi x)\, dx$.

noncomputable def HeatEquation.fourierSinePartialSum (f : ℝ → ℝ) (N : ℕ) (x : ℝ) : ℝ

The $N$-th partial Fourier sine series of $f$: $\sum_{m=1}^N A_m \sin(m \pi x)$.

noncomputable def HeatEquation.L2NormSq (f : ℝ → ℝ) : ℝ

The squared $L^2([0, 1])$ norm: $\|f\|_{L^2}^2 = \int_0^1 |f(x)|^2\, dx$.

noncomputable def HeatEquation.L2ErrorSq (f : ℝ → ℝ) (N : ℕ) : ℝ

The squared $L^2([0, 1])$ error between $f$ and its $N$-th Fourier sine partial sum.

noncomputable def HeatEquation.eigenvalue (m : ℕ) : ℝ

The $m$-th eigenvalue of $-\partial_x^2$ with Dirichlet conditions on $[0, 1]$: $-m^2 \pi^2$.

theorem HeatEquation.fourier_sine_theorem (f : ℝ → ℝ) (hf : MeasureTheory.Integrable (fun (x : ℝ) => f x ^ 2) (MeasureTheory.volume.restrict (Set.Icc 0 1))) : Filter.Tendsto (fun (N : ℕ) => L2ErrorSq f N) Filter.atTop (nhds 0) ∧ L2NormSq f = ∑' (m : ℕ), 1 / 2 * 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 - 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 HeatEquation.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 - fourierSinePartialSum f N x|) Filter.atTop (nhds 0)

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