OAI/Geometry/RCD/Harmonic/TwoCenterDirectionEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.two_center_direction_estimate line 20

   Source documentation

   The term involving the unknown matrix difference is absorbed using the small radial value error. The resulting direction estimate uses the same representatives as the two radial fits.

   theorem two_center_direction_estimate {K : ℝ} {n : ℕ}
       {hX : NoncollapsedRCD K n X}
       (hgradient : LocalHarmonicL2GradientInput hX)
       (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
       {κ : ℝ} (hκ : 0 ≤ κ) :
       ∃ Cg Cm : ℝ, 1 ≤ Cg ∧ 1 ≤ Cm ∧
       ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
       ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
         (V : X → Euclidean n) (N : Euclidean n ≃L[ℝ] Euclidean n),
       IsExactMeanNormalization (hausdorff n X) hX.quadratic
         (sobolevColumnMap (hausdorff n X) hX.quadratic u)
         (ball p (R / 2)) measurableSet_ball N →
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap