OAI/Analysis/AffineBernstein/WeightedPoincare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.compact_integrable_pair line 16
2. lemma OAI.AffineBernstein.integral_affine_convex_le line 26
3. lemma OAI.AffineBernstein.double_integral_segment_le line 51
4. lemma OAI.AffineBernstein.average_segment_energy_le line 87
5. theorem OAI.AffineBernstein.weighted_poincare line 110

   Source documentation

   Weighted Poincare in a compact convex set. The constant uses only chordal oscillation of the convex gradient, not pointwise ellipticity.

   theorem weighted_poincare {n : ℕ} {u f : Space n → ℝ}
       (hu : ContDiff ℝ ∞ u) (hf : ContDiff ℝ ∞ f) (hp : ∀ x, (hessian u x).PosDef)
       {K : Set (Space n)} (hK : IsCompact K) (hc : Convex ℝ K) {A : ℝ} (hA : 0 ≤ A)
       (hchord : ∀ x ∈ K, ∀ y ∈ K, (fderiv ℝ u y-fderiv ℝ u x) (y-x) ≤ A) :
       (∫ x in K, ∫ y in K, (f y-f x)^2) ≤
         A*((volume K).toReal * (2:ℝ)^n * ∫ x in K, inverseHessianPair u f f x) := by
   …

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