OAI/Geometry/RCD/Coordinates/RegularProjectionConfiguration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.regular_projection_configuration_constants line 19

   Source documentation

   The actual radial rows construct the full projection data. The affine constant is fixed before the measured error and every geometric choice.

   theorem regular_projection_configuration_constants {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
       (hgradient : LocalHarmonicL2GradientInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
       (hmeasured : LocalMeasuredCoordinateInput hX)
       {κ B J C A Cχ epsilon D : ℝ}
       (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hCχ : 0 ≤ Cχ)
       (hepsilon : 0 ≤ epsilon)
       (hsmall : ((m + 2 : ℕ) : ℝ) ^ 2 *
         (((5 / 3 : ℝ) * (16384 : ℝ) ^ (m + 2)) * epsilon) ≤ 1 / 2) :
       ∃ H : ℝ, 0 ≤ H ∧ ∀ error : ℝ, 0 < error → ∃ delta : ℝ, 0 < delta ∧
       ∀ {base first center : X} {a enlargement zeta eta Cg Ca : ℝ}
         {ker : ℝ → X → X → ℝ}
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput