OAI/Geometry/RCD/Coordinates/DyadicNormalizedFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_dyadic_normalized_family line 17

   Source documentation

   The all-small-scales transformation theorem supplies a single chosen family with exact means at the radii of the actual heat construction.

   theorem exists_dyadic_normalized_family (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
       {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (p : X) {R T β : ℝ}
       (hR : 0 < R) (hRT : 4 * R ≤ T)
       (hfamily : ∀ r : ℝ, 0 < r → 64 * r ≤ T →
         ∃ A : Euclidean n ≃L[ℝ] Euclidean n,
           IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
             (ball p (16 * r)) measurableSet_ball A ∧
           ∃ w : X → Euclidean n,
             FirstOrderSplittingOn μ hQ p (16 * r) β (transformedColumn μ hQ u A) w) :
       ∃ S : ℕ → Euclidean n ≃L[ℝ] Euclidean n,
         (∀ i, IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
           (ball p (R / 2 ^ i)) measurableSet_ball (S i)) ∧
   …

   Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn