OAI/Geometry/RCD/Harmonic/DyadicDistanceReplacements.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.curvature_lower_bound_mono line 14
2. structure OAI.RegularPointCoordinates.DyadicDistanceReplacements line 26

   Source documentation

   These are actual solutions for the sources in S, not replacement existence or error estimates supplied as additional assumptions.

   structure DyadicDistanceReplacements {n : ℕ} {κ r0 : ℝ} {p : X}
       (S : DyadicDistanceSources μ hQ n κ p r0) (B J C : ℝ) where
   …

   Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources

3. theorem OAI.RegularPointCoordinates.dyadic_distance_replacements_of_published line 65

   Source documentation

   The constants precede the center, root radius and selected source family, allowing the same constants in the two-center radial argument.

   theorem dyadic_distance_replacements_of_published {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
       (hsobolev : LocalDirichletSobolevInput hX) (hcutoff : LocalGoodCutoffInput hX)
       {κ : ℝ} (hκ : 0 ≤ κ) :
       letI : IsLocallyFiniteMeasure (hausdorff n X) :=
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalDirichletSobolevInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.hausdorff