OAI/Geometry/RCD/Coordinates/RadialMatrixEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.RadialMatrixEstimates line 17

   Source documentation

   The estimates already proved for the actual Poisson radial matrices, packaged only to retain their common choices of rows.

   def RadialMatrixEstimates {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
       [IsFiniteMeasureOnCompacts (hausdorff n X)]
       {κ r0 B J C Cχ : ℝ} {p : X}
       (S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0)
       (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
       (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (V : X → Euclidean n)
       (F : ℕ → Euclidean n ≃L[ℝ] Euclidean n)
       (χ : ∀ i, GoodLaplacianCutoff (hausdorff n X) hX.quadratic p (distanceSourceRadius r0 i / 64) Cχ)
       (δ Cg D Ca A : ℝ) : Prop :=
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.distanceSourceRadius