DyadicAffineCoefficient.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Affine nondegeneracy in the actual dyadic normalizing frame

theorem OAI.RegularPointCoordinates.dyadic_affine_coefficient line 19
Source documentation
The exact normalization eight levels inward controls the coefficients on the radial testing ball. Slow frame growth returns the estimate to the frame used by the radial fit, with a constant independent of scale.
```
theorem dyadic_affine_coefficient {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X)
    (hgradient : LocalHarmonicL2GradientInput hX)
    {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ {a R ε : ℝ}, 0 ≤ a → 0 < R → a * (3 * R) ≤ 1 →
      BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a) →
      ∀ p : X,
      ∀ (u : Fin (m + 2) → SobolevSpace (hausdorff (m + 2) X) hX.quadratic),
      ∀ F : ℕ → Euclidean (m + 2) ≃L[ℝ] Euclidean (m + 2),
      0 ≤ ε → ((m + 2 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio (m + 1) * ε) ≤ 1 / 64 →
      (∀ i, IsExactMeanNormalization (hausdorff (m + 2) X) hX.quadratic
        (sobolevColumnMap (hausdorff (m + 2) X) hX.quadratic u)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizationVolumeRatio, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap