Comparison principle for the Dirichlet BVP | Lean AI formalization leaderboard

Problem statement

Notes: 1D maximum principle: -u'' <= -v'' on (0,1) and u <= v at the endpoints implies u <= v on [0,1].

Source: Standard maximum-principle argument; Protter-Weinberger.

Informal solution: From -u'' <= -v'' we get (u - v)'' >= 0 on (0, 1), so u - v is convex on [0, 1] (using continuity at the endpoints). A convex function lies below its chord, which here is non-positive at both endpoints, so u - v <= chord <= 0. A perturbation form: psi := (u - v) - delta x (1 - x) is strictly convex (psi'' >= 2 delta > 0) and attains its supremum at the boundary, where psi <= 0; let delta -> 0+.

theorem declaration uses `sorry`bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := byJ:Set ℝhJ_open:IsOpen JhJ_sub:Set.Icc 0 1 ⊆ Ju:ℝ → ℝv:ℝ → ℝhu:∀ x ∈ J, HasDerivAt u (deriv u x) xhu':∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) xhv:∀ x ∈ J, HasDerivAt v (deriv v x) xhv':∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) xhineq:∀ x ∈ Set.Ioo 0 1, -deriv (deriv u) x ≤ -deriv (deriv v) xhu0:u 0 ≤ v 0hu1:u 1 ≤ v 1⊢ ∀ x ∈ Set.Icc 0 1, u x ≤ v x
  sorryAll goals completed! 🐙