structure HeatUniqueness.IsHeatSolution (T L : ℝ) (f : ℝ → ℝ → ℝ) (g α β : ℝ → ℝ) (u : ℝ → ℝ → ℝ) : Prop

A predicate asserting that $u : [0, T] \times [0, L] \to \mathbb{R}$ is a classical solution to the inhomogeneous heat equation $u_t - u_{xx} = f(t, x)$ with initial condition $u(0, x) = g(x)$ and Dirichlet boundary conditions $u(t, 0) = \alpha(t)$, $u(t, L) = \beta(t)$, together with the regularity (continuity and differentiability) hypotheses needed for the uniqueness argument via the energy method.

• pde (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ x ∈ Set.Ioo 0 L, deriv (fun (x_1 : ℝ) => u x_1 x) t - deriv (deriv fun (x : ℝ) => u t x) x = f t x
• initial (x : ℝ) : x ∈ Set.Icc 0 L → u 0 x = g x
• left_bc (t : ℝ) : t ∈ Set.Icc 0 T → u t 0 = α t
• right_bc (t : ℝ) : t ∈ Set.Icc 0 T → u t L = β t
• cont : ContinuousOn (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Icc 0 T ×ˢ Set.Icc 0 L)
• diffT (t : ℝ) : t ∈ Set.Icc 0 T → ∀ x ∈ Set.Icc 0 L, DifferentiableAt ℝ (fun (x_1 : ℝ) => u x_1 x) t
• diffX (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ x ∈ Set.Ioo 0 L, DifferentiableAt ℝ (fun (x : ℝ) => u t x) x
• diffXX (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ x ∈ Set.Ioo 0 L, DifferentiableAt ℝ (deriv fun (x : ℝ) => u t x) x
• contDerivT : ContinuousOn (fun (p : ℝ × ℝ) => deriv (fun (x : ℝ) => u x p.2) p.1) (Set.Icc 0 T ×ˢ Set.Icc 0 L)
• diffXGlobal (t : ℝ) : t ∈ Set.Ioo 0 T → Differentiable ℝ fun (x : ℝ) => u t x
• diffXXGlobal (t : ℝ) : t ∈ Set.Ioo 0 T → Differentiable ℝ (deriv fun (x : ℝ) => u t x)
• contDerivX (t : ℝ) : t ∈ Set.Ioo 0 T → ContinuousOn (deriv fun (x : ℝ) => u t x) (Set.Icc 0 L)
• contDerivXX (t : ℝ) : t ∈ Set.Ioo 0 T → ContinuousOn (deriv (deriv fun (x : ℝ) => u t x)) (Set.Icc 0 L)

noncomputable def HeatUniqueness.energy (w : ℝ → ℝ → ℝ) (L t : ℝ) : ℝ

The $L^2$ energy of $w(t, \cdot)$ on $[0, L]$ at time $t$: $E(t) = \int_0^L w(t, x)^2\, dx$. Used in the energy-method uniqueness proof.