OAI/Analysis/AffineBernstein/LogCaccioppoli.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.contDiff_cofactorHessian_entry_global line 16
2. lemma OAI.AffineBernstein.integral_flux_compact line 24
3. lemma OAI.AffineBernstein.inverseHessian_ibp line 43
4. lemma OAI.AffineBernstein.contDiff_inverseHessianTrace_global line 89
5. lemma OAI.AffineBernstein.contDiff_inverseHessianPair_global line 103
6. lemma OAI.AffineBernstein.inverseHessianPair_cauchy line 118
7. lemma OAI.AffineBernstein.inverseHessianTrace_log_supersolution line 136
8. theorem OAI.AffineBernstein.linearizedMA_log_caccioppoli line 163

   Source documentation

   Caccioppoli for the logarithm of a strictly positive supersolution of the actual cofactor-divergence operator. The coefficients are not assumed uniformly elliptic, and no Harnack estimate enters this proof.

   theorem linearizedMA_log_caccioppoli {n : ℕ} {u s η : Space n → ℝ}
       (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
       (hs : ContDiff ℝ ∞ s) (hpos : ∀ x, 0 < s x)
       (hL : ∀ x, inverseHessianTrace u s x ≤ 0)
       (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η) :
       (∫ x, (hessian u x).det * (η x)^2 *
         inverseHessianPair u (fun y => Real.log (s y)) (fun y => Real.log (s y)) x) ≤
         4 * ∫ x, (hessian u x).det * inverseHessianPair u η η x := by
   …

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