ControlledNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization retaining arbitrarily small splitting error

The two published harmonic inputs are applied with compatible thresholds. Metric flatness supplies the no-extra-factor hypothesis by a proved finite configuration argument. The resulting normalization acts on the actual Sobolev column, and its pointwise coordinate map approximates the metric.

theorem OAI.RegularPointCoordinates.controlled_scaled_curvature_lower line 20

theorem OAI.RegularPointCoordinates.controlled_normalization_of_published_inputs line 36

Source documentation

A common threshold retains exact means, the prescribed first-order error, and metric approximation at every interior scale. The extra quantitative conclusion is already present in Huang--Huang Theorem 4.1(1).

theorem controlled_normalization_of_published_inputs {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (htrans : LocalTransformationInput hX) (hsplit : LocalFlatSplittingInput hX)
    {ρ β : ℝ} (hρ : 0 < ρ) (hβ : 0 < β) :
    ∃ δ : ℝ, 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 →
        (∀ s : ℝ, 0 < s → s ≤ R →
          ∃ f : X → Euclidean n, IsPointedApproximation p 0 s 2 δ f) →
        ∀ r : ℝ, 0 < r → 16 * r ≤ R → ∃ A : Euclidean n ≃L[ℝ] Euclidean n,
          IsExactMeanNormalization (hausdorff n X) hX.quadratic
            (sobolevColumnMap (hausdorff n X) hX.quadratic u)
…

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, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap