Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Corollaries of comparison

This file records elementary consequences of the comparison theorems.

theorem ViscositySolns.eqOn_of_comparisonConclusions {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} (huv : ComparisonConclusionOn C u v) (hvu : ComparisonConclusionOn C v u) : Set.EqOn u v C

Two comparison inequalities give equality on the domain.

In quantified mathematical form, if u x ≤ v x and v x ≤ u x for every x ∈ C, then u x = v x for every x ∈ C.

theorem ViscositySolns.ViscositySolution.eqOn_of_comparisonConclusions {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} (_hu : ViscositySolution C F u) (_hv : ViscositySolution C F v) (huv : ComparisonConclusionOn C u v) (hvu : ComparisonConclusionOn C v u) : Set.EqOn u v C

Uniqueness of viscosity solutions once comparison has been proved in both directions.

In quantified mathematical form, let u and v be viscosity solutions of the same equation F = 0 on C. If comparison gives u x ≤ v x for every x ∈ C and also gives v x ≤ u x for every x ∈ C, then u x = v x for every x ∈ C.