WorkingNormalizerBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded working frame from a near-identity mean Gram

theorem OAI.RegularPointCoordinates.normalizer_norm_sq_le_two_of_sub_id line 20
Source documentation
Every exact normalizer of a mean Gram within one half of the identity has squared norm at most two. This is uniform in the chosen normalizer.
```
theorem normalizer_norm_sq_le_two_of_sub_id (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    (U : E →L[ℝ] SobolevSpace μ hQ) (s : Set X) (hs : MeasurableSet s)
    (A : E ≃L[ℝ] E) (hA : IsExactMeanNormalization μ hQ U s hs A)
    (hgram : ‖sobolevMeanGram μ hQ U s hs - ContinuousLinearMap.id ℝ E‖ ≤ 1 / 2) :
    ‖(A : E →L[ℝ] E)‖ ^ 2 ≤ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.exists_nearby_working_normalizer line 40

Source documentation

The initial splitting error and the fixed Bishop--Gromov volume ratio construct uniformly bounded working frames at every nearby center.

theorem exists_nearby_working_normalizer {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
    {p q : X} {R ε : ℝ} {w : X → Euclidean (m + 1)}
    (hR : 0 < R) (hscale : a * (3 * R) ≤ 1) (hε : 0 ≤ ε)
    (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 2)
    (hfirst : FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p (2 * R) ε u w)
    (hq : q ∈ Metric.ball p (R / 4)) :
    ∃ T : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1),
      IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
        (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizationVolumeRatio, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap