OAI/Geometry/RCD/Sobolev/AnnularPoincare.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.annularPoincareConstant line 15
2. theorem OAI.RegularPointCoordinates.annularPoincareConstant_pos line 18
3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.annular_dirichlet_poincare line 25

   Source documentation

   Doubling of the volume between r and 2r provides enough zero boundary outside B(r). The transport estimate then gives one constant for all r<=1.

   theorem NoncollapsedRCD.annular_dirichlet_poincare {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) {r : ℝ}
       (hr : 0 < r) (hr1 : r ≤ 1)
       (hvol : 0 < (hausdorff n X).real (ball p r))
       (hdouble : 2 * (hausdorff n X).real (ball p r) ≤
         (hausdorff n X).real (ball p (2 * r)))
       (f : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball p r)) :
       ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic f.val‖ ^ 2 ≤
         (annularPoincareConstant K n * r ^ 2) * energyForm (hausdorff n X) hX.quadratic f.val f.val := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.annularPoincareConstant, OAI.RegularPointCoordinates.energyForm