SplittingApproximation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

First-order splitting maps and the published almost-splitting input

LocalAlmostSplittingInput is a specialization of Huang--Huang (2024), Theorem 2.9(2), with the first-order criterion following Definition 2.7. The first-order data are imposed on B_(16r); the conclusion concerns B_(2r), leaving the factor two needed for the criterion. Threshold losses include metric rescaling and the conversion from GH isometries to pointed maps.

The consequence proved here eliminates the residual product factor when there is also a Euclidean approximation. No bi-Lipschitz or injectivity conclusion is included in the published premise.

structure OAI.RegularPointCoordinates.FirstOrderSplittingOn line 35
Source documentation
The first-order conditions of Huang--Huang Definition 2.7, on actual Sobolev components with continuous pointwise representatives. The Hessian condition is obtained on a smaller ball by the published following remark.
```
structure FirstOrderSplittingOn {n : ℕ} (p : X) (r ε : ℝ)
    (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n) : Prop where
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.LocalAlmostSplittingInput line 48
Source documentation
The precise product-map consequence used from Huang--Huang Theorem 2.9(2) and its first-order criterion, including the residual product factor.
```
def LocalAlmostSplittingInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
def OAI.RegularPointCoordinates.LocalFlatSplittingInput line 61
Source documentation
Only this Euclidean-flat coordinate consequence of the product theorem is used in the chart construction. It is also proved directly from the noncollapsed measured-coordinate input in FlatSplittingApproximation.
```
def LocalFlatSplittingInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.IsPointedApproximation.mono_error line 72
Source documentation
Increasing the error preserves a pointed approximation, including its smaller target-density requirement.
```
theorem IsPointedApproximation.mono_error {Y : Type*} [MetricSpace Y]
    {p : X} {q : Y} {r R ε δ : ℝ} {f : X → Y}
    (hf : IsPointedApproximation p q r R ε f) (hεδ : ε ≤ δ) :
    IsPointedApproximation p q r R δ f := by
…
```
Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.splitting_coordinates_approximate line 84

Source documentation

Almost splitting plus metric flatness controls the actual harmonic coordinates. The tolerances are uniform in the center, scale and map.

theorem splitting_coordinates_approximate {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (hpublished : LocalAlmostSplittingInput hX)
    {ρ : ℝ} (hρ : 0 < ρ) :
    ∃ τ ε : ℝ, 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 (16 * r) ε u v →
          (∃ f : X → Euclidean n, IsPointedApproximation p 0 r 2 τ f) →
          IsPointedApproximation p 0 r (1 / 2) ρ (fun x => r⁻¹ • (v x - v p)) := by
…

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

theorem OAI.RegularPointCoordinates.LocalAlmostSplittingInput.flatSplittingInput line 111