OAI/Geometry/RCD/Coordinates/DyadicRadialFit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.dyadicRadialFit line 19

   Source documentation

   The bound only supplies local L2 membership. The numerical value is the actual least-squares residual for the canonical distance derivative.

   def dyadicRadialFit {κ r0 B J 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) (L : ℝ)
       (hbase : ∀ i j, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (distanceSourceRadius r0 i / 64)),
         localGamma (hausdorff n X) hX.quadratic (u j) (u j) x ≤ L ^ 2)
       (i : ℕ) (b : Euclidean n) : ℝ :=
   …

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

2. theorem OAI.RegularPointCoordinates.dyadicRadialFit_nonneg line 32