FiniteNormalizerGrowth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial norm control of exact normalizers over a finite range

theorem OAI.RegularPointCoordinates.normalizer_norm_sq_le_of_mean_growth line 19

Source documentation

Relative growth of means gives the squared norm bound for the exact normalizer at the smaller scale. The larger mean is already normalized.

theorem normalizer_norm_sq_le_of_mean_growth (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    (U : E →L[ℝ] SobolevSpace μ hQ) (s t : Set X)
    (hs : MeasurableSet s) (ht : MeasurableSet t)
    (A : E ≃L[ℝ] E) (hA : IsExactMeanNormalization μ hQ U s hs A)
    (htId : sobolevMeanGram μ hQ U t ht = ContinuousLinearMap.id ℝ E)
    {B : ℝ} (hB : 0 ≤ B)
    (hgrowth : ∀ v : E, ⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ ≤
      B * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ) :
    ‖(A : E →L[ℝ] E)‖ ^ 2 ≤ B := by
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.norm_apply_sq_le_of_norm_sq_le line 45
Source documentation
The frame growth bound yields a bound for every transformed direction.
```
theorem norm_apply_sq_le_of_norm_sq_le (A : E →L[ℝ] E) {B : ℝ}
    (hA : ‖A‖ ^ 2 ≤ B) (v : E) : ‖A v‖ ^ 2 ≤ B * ‖v‖ ^ 2 := by
…
```

theorem OAI.RegularPointCoordinates.dyadic_normalizer_norm_sq_bound line 54

Source documentation

A normalized working-scale mean gives polynomial growth of every smaller exact frame from the proved adjacent mean comparisons.

theorem dyadic_normalizer_norm_sq_bound {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 : X) {r ε : ℝ} (hr : 0 < r) (hε : 0 ≤ ε)
    (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 2)
    (A : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
    (hA : IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
      (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u) (ball p r) measurableSet_ball A)
    (k : ℕ) (hscale : ∀ j ≤ k, a * (3 * (2 ^ j * r)) ≤ 1)
    (hnormal : ∀ j ≤ k, ∃ (S : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
      (w : X → Euclidean (m + 1)),
…

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