OAI/Geometry/RCD/Coordinates/CenteredSplitting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.centeredColumn line 22
2. theorem OAI.RegularPointCoordinates.centeredColumn_apply line 27
3. theorem OAI.RegularPointCoordinates.centeredColumn_representative line 35
4. theorem OAI.RegularPointCoordinates.centeredColumn_difference line 51
5. theorem OAI.RegularPointCoordinates.centeredColumn_gram line 64
6. theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.center line 77
7. theorem OAI.RegularPointCoordinates.centeredColumn_residual line 104
8. theorem OAI.RegularPointCoordinates.centeredColumn_covector_difference line 112
9. theorem OAI.RegularPointCoordinates.centeredColumn_radial_fit line 132

   Source documentation

   The raw derivative and its affine fit are unchanged by centering, for every fixed covector and every admissible local gradient bound.

   theorem centeredColumn_radial_fit {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
       (p : X) (r : ℝ) (hfin : μ (ball p r) ≠ ∞) (c b : Euclidean n)
       (η q : SobolevSpace μ hQ)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict (ball p r)] fun _ => (1 : ℝ))
       {B B' : ℝ}
       (ha : ∀ᵐ x ∂μ.restrict (ball p r),
         localGamma μ hQ (sobolevColumnMap μ hQ (centeredColumn μ hQ u c η) b)
           (sobolevColumnMap μ hQ (centeredColumn μ hQ u c η) b) x ≤ B)
       (ha' : ∀ᵐ x ∂μ.restrict (ball p r),
         localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤ B') :
       radialFitError μ hQ (centeredColumn μ hQ u c η) p r hfin q
         (sobolevColumnMap μ hQ (centeredColumn μ hQ u c η) b) ha =
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredColumn, OAI.RegularPointCoordinates.radialFitError