UniformControlledNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform normalization at nearby centers

A single harmonic map on the enlarged initial ball supplies the maps at all nearby centers. Only the volume-ratio cost is paid when its first-order splitting data are restricted. The resulting normalizers and approximation bounds are uniform in the center and in every smaller scale.

theorem OAI.RegularPointCoordinates.uniform_controlled_coordinates line 27

Source documentation

Uniform first-order data and all-center flatness give actual normalized harmonic coordinates at every center in the inner quarter-ball.

theorem uniform_controlled_coordinates {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (htrans : LocalTransformationInput hX) (hsplit : LocalFlatSplittingInput hX)
    {ρ β C : ℝ} (hρ : 0 < ρ) (hβ : 0 < β) (hC : 1 ≤ C) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (p : X) (R : ℝ), 0 < R → -δ ≤ K * R ^ 2 →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (v : X → Euclidean n),
        FirstOrderSplittingOn (hausdorff n X) hX.quadratic p (2 * R) δ u v →
        (∀ q ∈ ball p (R / 4),
          (hausdorff n X).real (ball p (2 * R)) ≤
            C * (hausdorff n X).real (ball q (R / 2))) →
        (∀ q ∈ ball p (R / 4), ∀ s : ℝ, 0 < s → s ≤ R / 4 →
          ∃ f : X → Euclidean n, IsPointedApproximation q 0 s 2 δ f) →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.uniform_controlled_coordinates_of_comparison line 93

Source documentation

The volume-ratio premise is supplied by Bishop--Gromov with a fixed constant depending only on dimension.

theorem uniform_controlled_coordinates_of_comparison {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) (hn : 2 ≤ m + 1)
    (htrans : LocalTransformationInput hX) (hsplit : LocalFlatSplittingInput hX)
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    {ρ β : ℝ} (hρ : 0 < ρ) (hβ : 0 < β) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (p : X) (R : ℝ), 0 < R → -δ ≤ K * R ^ 2 →
      a * (3 * R) ≤ 1 →
      ∀ (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
        (v : X → Euclidean (m + 1)),
        FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p (2 * R) δ u v →
        (∀ q ∈ ball p (R / 4), ∀ s : ℝ, 0 < s → s ≤ R / 4 →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn