OAI/Geometry/RCD/Coordinates/NormalizedProjectionConfiguration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_projection_configuration line 22

   Source documentation

   Exact normalized, centered harmonic coordinates and the actual scalar row fits construct the sharp-projection configuration. The affine constant is chosen before the centers, scales, sources, and coordinate map.

   theorem normalized_projection_configuration {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hgradient : LocalHarmonicL2GradientInput hX)
       (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
       {κ B J C A Cχ epsilon Drow : ℝ} (hκ : 0 ≤ κ) (hepsilon : 0 ≤ epsilon)
       (hDrow : 0 ≤ Drow)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (16384 : ℝ) ^ n) * epsilon) ≤ 1 / 2) :
       ∃ H : ℝ, 0 ≤ H ∧ ∀ (root : ℝ) (first center : X)
         (S1 : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ first root)
         (S2 : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ center root)
         (T1 : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S1 B J C)
         (T2 : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S2 B J C) (i : ℕ),
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements