The Maximum Principle for the Heat Equation on a Finite Interval

Main Result

• heat_maximum_principle_finite_interval: The (weak) maximum principle states that the maximum value of a solution to the heat equation on a finite space-time domain agrees with either the maximum at the initial time or on the spatial boundary.

References

This formalizes Theorem 7.7.

def HeatEquation.Ω_T (l T : ℝ) : Set (ℝ × ℝ)

Equations

• HeatEquation.Ω_T l T = Set.Icc 0 l ×ˢ Set.Icc 0 T

def HeatEquation.S_boundary (l T : ℝ) : Set (ℝ × ℝ)

Equations

• HeatEquation.S_boundary l T = Set.Icc 0 l ×ˢ {0} ∪ {0} ×ˢ Set.Icc 0 T ∪ {l} ×ˢ Set.Icc 0 T

def HeatEquation.Top_Edge (l T : ℝ) : Set (ℝ × ℝ)

Equations

• HeatEquation.Top_Edge l T = Set.Ioo 0 l ×ˢ {T}

def HeatEquation.Interior (l T : ℝ) : Set (ℝ × ℝ)

Equations

• HeatEquation.Interior l T = Set.Ioo 0 l ×ˢ Set.Ioo 0 T

theorem HeatEquation.local_max_implies_second_deriv_nonpos {f : ℝ → ℝ} {x₀ : ℝ} (h_smooth : ContDiffAt ℝ 2 f x₀) (h_max : IsLocalMax f x₀) : deriv f x₀ = 0 ∧ deriv (deriv f) x₀ ≤ 0

theorem HeatEquation.isLocalMin_of_iteratedFDeriv {f : ℝ → ℝ} {x₀ : ℝ} (hf : ((iteratedFDeriv ℝ 2 f x₀) fun (x : Fin 2) => 1) > 0) (hd : deriv f x₀ = 0) (hc : ContinuousAt f x₀) : IsLocalMin f x₀

theorem HeatEquation.hΩ {l T : ℝ} (hl : 0 < l) (hT : 0 < T) : UniqueDiffOn ℝ (Ω_T l T)

theorem HeatEquation.h_int_nhds {l T : ℝ} (p : ℝ × ℝ) : p ∈ Interior l T → Ω_T l T ∈ nhds p

theorem HeatEquation.perturb_dt {l T ε : ℝ} {u v : ℝ → ℝ → ℝ} (hv_def : v = fun (x t : ℝ) => u x t + ε * x ^ 2) (x t : ℝ) : (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => v x t') t = deriv (fun (t' : ℝ) => u x t') t

theorem HeatEquation.perturb_dxx {l T ε : ℝ} {u v : ℝ → ℝ → ℝ} (hv_def : v = fun (x t : ℝ) => u x t + ε * x ^ 2) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (x t : ℝ) : (x, t) ∈ Interior l T → deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => v x'' t) x') x = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x + 2 * ε

theorem HeatEquation.heat_equation_perturbation_ineq {l T α ε : ℝ} {u v : ℝ → ℝ → ℝ} (hα : 0 < α) (hε : 0 < ε) (hv_def : v = fun (x t : ℝ) => u x t + ε * x ^ 2) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (h_pde : ∀ (x t : ℝ), (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => u x t') t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x) (x t : ℝ) : (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => v x t') t - α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => v x'' t) x') x < 0

theorem HeatEquation.iteratedFDeriv_two_eval_xx_eq_iteratedDeriv_slice {u : ℝ → ℝ → ℝ} {x₀ t : ℝ} (hF : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u p.1 p.2) : (iteratedFDeriv ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (x₀, t)) ![(1, 0), (1, 0)] = iteratedDeriv 2 (fun (x' : ℝ) => u x' t) x₀

theorem HeatEquation.u_xx_conti_Ω_T (l T : ℝ) {u : ℝ → ℝ → ℝ} (hT : 0 < T) (hl : 0 < l) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) : ContinuousOn (fun (p : ℝ × ℝ) => (iteratedFDerivWithin ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T) p) ![(1, 0), (1, 0)]) (Ω_T l T)

theorem HeatEquation.u_xx_continuous {l T x₀ : ℝ} {u : ℝ → ℝ → ℝ} (hT : 0 < T) (hl : 0 < l) (hx_pos : 0 < x₀) (hx_lt : x₀ < l) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) : ContinuousWithinAt (fun (t : ℝ) => deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x₀) (Set.Iic T) T

theorem HeatEquation.u_t_continuous {l T x₀ : ℝ} {u : ℝ → ℝ → ℝ} (hT : 0 < T) (hx_pos : 0 < x₀) (hx_lt : x₀ < l) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) : ContinuousWithinAt (fun (t : ℝ) => derivWithin (fun (s : ℝ) => u x₀ s) (Set.Iic T) t) (Set.Iic T) T

theorem HeatEquation.pde_boundary_val {l T α ε x₀ : ℝ} {u : ℝ → ℝ → ℝ} (hT : 0 < T) (hl : 0 < l) (hx_pos : 0 < x₀) (hx_lt : x₀ < l) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (h_pde : ∀ (x t : ℝ), (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => u x t') t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x) : have v := fun (x t : ℝ) => u x t + ε * x ^ 2; derivWithin (fun (t : ℝ) => v x₀ t) (Set.Iic T) T - α * deriv (fun (x : ℝ) => deriv (fun (y : ℝ) => v y T) x) x₀ = -2 * α * ε

theorem HeatEquation.heat_equation_no_interior_max {l T α ε : ℝ} {u v : ℝ → ℝ → ℝ} (hα : 0 < α) (hv_def : v = fun (x t : ℝ) => u x t + ε * x ^ 2) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (h_int_nhds : ∀ p ∈ Interior l T, Ω_T l T ∈ nhds p) (h_v_pde_ineq : ∀ (x t : ℝ), (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => v x t') t - α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => v x'' t) x') x < 0) (x₀ t₀ : ℝ) : (x₀, t₀) ∈ Interior l T → ¬IsMaxOn (fun (p : ℝ × ℝ) => v p.1 p.2) (Ω_T l T) (x₀, t₀)

theorem HeatEquation.deriv_nonneg_of_isLocalMaxOn_Icc_right {f : ℝ → ℝ} {T : ℝ} (hT : 0 < T) (hC1 : ContDiffOn ℝ 1 f (Set.Icc 0 T)) (hmax : IsLocalMaxOn f (Set.Icc 0 T) T) : 0 ≤ derivWithin f (Set.Icc 0 T) T

theorem HeatEquation.Omega_T_decompose {l T : ℝ} {p : ℝ × ℝ} (hp : p ∈ Ω_T l T) : p ∈ S_boundary l T ∨ p ∈ Interior l T ∨ p ∈ Top_Edge l T

theorem HeatEquation.heat_equation_no_top_edge_max {l T α ε : ℝ} {u v : ℝ → ℝ → ℝ} (hT : 0 < T) (hl : 0 < l) (hα : 0 < α) (hε : 0 < ε) (hv_def : v = fun (x t : ℝ) => u x t + ε * x ^ 2) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (h_pde : ∀ (x t : ℝ), (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => u x t') t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x) (x₀ : ℝ) : 0 < x₀ → x₀ < l → ¬IsMaxOn (fun (p : ℝ × ℝ) => v p.1 p.2) (Ω_T l T) (x₀, T)

theorem HeatEquation.max_v_on_S_boundary {l T : ℝ} {v : ℝ → ℝ → ℝ} (hT : 0 < T) (h_compact : IsCompact (Ω_T l T)) (h_nonempty : (Ω_T l T).Nonempty) (h_v_cont : ContinuousOn (fun (p : ℝ × ℝ) => v p.1 p.2) (Ω_T l T)) (h_no_int : ∀ (x₀ t₀ : ℝ), (x₀, t₀) ∈ Interior l T → ¬IsMaxOn (fun (p : ℝ × ℝ) => v p.1 p.2) (Ω_T l T) (x₀, t₀)) (h_no_top : ∀ (x₀ : ℝ), 0 < x₀ → x₀ < l → ¬IsMaxOn (fun (p : ℝ × ℝ) => v p.1 p.2) (Ω_T l T) (x₀, T)) : ∃ s_max ∈ S_boundary l T, ∀ p ∈ Ω_T l T, v p.1 p.2 ≤ v s_max.1 s_max.2

theorem HeatEquation.heat_equation_max_principle (l T α : ℝ) (u : ℝ → ℝ → ℝ) (hl : 0 < l) (hT : 0 < T) (hα : 0 < α) (h_smooth : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Ω_T l T)) (h_pde : ∀ (x t : ℝ), (x, t) ∈ Interior l T → deriv (fun (t' : ℝ) => u x t') t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u x'' t) x') x) : sSup ((fun (p : ℝ × ℝ) => u p.1 p.2) '' Ω_T l T) = sSup ((fun (p : ℝ × ℝ) => u p.1 p.2) '' S_boundary l T)