ProjectionAffineNormalization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Affine nondegeneracy at the two actual projection radii

theorem OAI.RegularPointCoordinates.projection_affine_bounds line 23

Source documentation

A splitting frame normalized on the large ball gives both affine bounds needed by the actual projection. The small-ball normalizer is constructed from the positive Gram, then compared to that same large frame.

theorem projection_affine_bounds {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
    {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ H : ℝ, 0 ≤ H ∧ ∀ (p : X) (s R : ℝ), 0 < s → s / 4096 ≤ R → R ≤ s →
      -κ ≤ K * R ^ 2 →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (V W : X → Euclidean n)
        (N : Euclidean n ≃L[ℝ] Euclidean n) (epsilon : ℝ), 0 ≤ epsilon →
      (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (16384 : ℝ) ^ n) * epsilon) ≤ 1 / 2 →
      (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p (2 * s)) (u j)) →
      ContinuousOn V (ball p (2 * s)) → V p = 0 →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn