Comparison principle for the Dirichlet BVP

bvp_comparison

Submitter: Kim Morrison.

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! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @kim-em with Aristotle (Harmonic) on May 2, 2026 (proof)

• @A-M-Berns with GPT-5.5 Codex on May 7, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 7, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @sqrt-of-2 with Gemini 3.1 Pro on May 10, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @rishistyping with Stealth Model on May 15, 2026

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026