OAI/Analysis/AffineBernstein/EllipticComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseHessianTrace_strict_maximum_principle line 20

   Source documentation

   Elementary strict comparison for the genuine inverse-Hessian operator. No quantitative elliptic regularity or Harnack estimate is used here.

   lemma inverseHessianTrace_strict_maximum_principle {n : ℕ}
       {u f : Space n → ℝ} {K : Set (Space n)} (hK : IsCompact K)
       (hf : ContinuousOn f K)
       (hs : ∀ x ∈ interior K, ContDiffAt ℝ ∞ f x)
       (hp : ∀ x ∈ interior K, (hessian u x).PosDef)
       (hL : ∀ x ∈ interior K, 0 < inverseHessianTrace u f x)
       (hb : ∀ x ∈ K, x ∉ interior K → f x ≤ 0) :
       ∀ x ∈ K, f x ≤ 0 := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.inverseHessianTrace

2. lemma OAI.AffineBernstein.inverseHessianTrace_sub line 39
3. lemma OAI.AffineBernstein.inverseHessianTrace_add_constant line 45
4. lemma OAI.AffineBernstein.inverseHessianTrace_sub_constant line 49