OAI/Geometry/RCD/Coordinates/NormalizedFrameRadialSmallness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.radialNormalizationRestrictionConstant line 15
2. theorem OAI.RegularPointCoordinates.radialNormalizationRestrictionConstant_ge_one line 17
3. theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.normalized_frame_fit_smallness line 29

   Source documentation

   The normalizing ball has radius twice the distance-source radius. Its first-order and metric estimates control the original radial fit on the testing ball with an explicit, scale-independent coefficient.

   theorem DyadicDistanceReplacements.normalized_frame_fit_smallness
       {n : ℕ} {κ r0 B J C omega δ Cχ : ℝ} {p : X}
       {S : DyadicDistanceSources μ hQ n κ p r0}
       (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
       (homega : 0 < omega) (hδ : 0 ≤ δ)
       (hδ1 : radialNormalizationRestrictionConstant n * δ ≤ 1) (hCχ : 0 ≤ Cχ)
       (hquarter : ∀ t : ℝ, 0 < t → t ≤ 2 * distanceSourceRadius r0 i →
         |μ.real (ball p t) / (omega * t ^ n) - 1| ≤ 1 / 4)
       (u : Fin n → SobolevSpace μ hQ) (A : Euclidean n ≃L[ℝ] Euclidean n)
       (v : X → Euclidean n)
       (hfirst : FirstOrderSplittingOn μ hQ p (2 * distanceSourceRadius r0 i) δ
         (transformedColumn μ hQ u A) v)
   …

   Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.radialNormalizationRestrictionConstant, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn