Maximum principle for a one-dimensional elliptic operator

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook

namespace LarssonThomee.Thm21

/-- The differential operator of (2.1): `𝒜u := -(a u')' + b u' + c u`, evaluated at `x`.
It is used only at points `x ∈ Ω = (0,1)`. There `u ∈ C²(Ω̄)` and the smooth coefficient `a`
make the classical derivatives below genuine. -/
def opA (a b c u : ℝ → ℝ) (x : ℝ) : ℝ :=
  -deriv (fun y => a y * deriv u y) x + b x * deriv u x + c x * u x

/-- Theorem 2.1 (maximum principle). This is for the operator `𝒜` of (2.1) on `Ω = (0,1)`.
The coefficients `a, b, c` are smooth on `Ω̄ = [0,1]`, and `a(x) ≥ a₀ > 0` on `Ω̄` as in (2.2).
We take `u ∈ C²(Ω̄)`. Then:
* If `𝒜u ≤ 0` in `Ω`:
  * (i) when `c = 0`, `max_{Ω̄} u = max{u(0), u(1)}`;
  * (ii) when `c ≥ 0` in `Ω`, `max_{Ω̄} u ≤ max{u(0), u(1), 0}`.
* If `𝒜u ≥ 0` in `Ω`, the corresponding `min` statements hold. -/
theorem maximum_principle
    (a b c u : ℝ → ℝ) (a₀ : ℝ)
    (ha : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) a (Set.Icc (0:ℝ) 1))
    (hb : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) b (Set.Icc (0:ℝ) 1))
    (hc : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) c (Set.Icc (0:ℝ) 1))
    (ha₀ : 0 < a₀) (ha_lb : ∀ x ∈ Set.Icc (0:ℝ) 1, a₀ ≤ a x)
    (hu : ContDiffOn ℝ 2 u (Set.Icc (0:ℝ) 1)) :
    ((∀ x ∈ Set.Ioo (0:ℝ) 1, opA a b c u x ≤ 0) →
      ((∀ x ∈ Set.Icc (0:ℝ) 1, c x = 0) →
          sSup (u '' Set.Icc (0:ℝ) 1) = max (u 0) (u 1)) ∧
      ((∀ x ∈ Set.Ioo (0:ℝ) 1, 0 ≤ c x) →
          sSup (u '' Set.Icc (0:ℝ) 1) ≤ max (max (u 0) (u 1)) 0)) ∧
    ((∀ x ∈ Set.Ioo (0:ℝ) 1, 0 ≤ opA a b c u x) →
      ((∀ x ∈ Set.Icc (0:ℝ) 1, c x = 0) →
          sInf (u '' Set.Icc (0:ℝ) 1) = min (u 0) (u 1)) ∧
      ((∀ x ∈ Set.Ioo (0:ℝ) 1, 0 ≤ c x) →
          min (min (u 0) (u 1)) 0 ≤ sInf (u '' Set.Icc (0:ℝ) 1))) := by
  sorry

end LarssonThomee.Thm21

end PDETextbook