OAI/Geometry/RCD/Coordinates/RegularPairCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bounded_exact_mean_normalization line 19

   Source documentation

   A half-unit Gram error constructs a bounded exact normalizer.

   theorem bounded_exact_mean_normalization (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
       {n : ℕ} (U : Euclidean n →L[ℝ] SobolevSpace μ hQ)
       (Ω : Set X) (hΩ : MeasurableSet Ω)
       (hsmall : ‖sobolevMeanGram μ hQ U Ω hΩ - ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤ 1 / 2) :
       ∃ N : Euclidean n ≃L[ℝ] Euclidean n,
         IsExactMeanNormalization μ hQ U Ω hΩ N ∧ ‖N.toContinuousLinearMap‖ ≤ 2 := by
   …

   Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.IsExactMeanNormalization

2. theorem OAI.RegularPointCoordinates.regular_pair_coordinates line 42

   Source documentation

   The interior normalization and coordinate size are consequences of the same actual splitting map used for both radial fits.

   theorem regular_pair_coordinates {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
       {base center : X} {a κ B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
       {ker : ℝ → X → X → ℝ}
       {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
       (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
       (hcenter : center ∈ ball base (e.heat.radius / 32))
       (d : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca center)
       (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1)
       (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (8192 : ℝ) ^ n) * zeta) ≤ 1 / 2)
       (i : ℕ) :
       let μ := hausdorff n X
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData