OAI/Geometry/RCD/Metric/PositiveSquaredDistance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A compact Sobolev representative of the positive squared distance

Adding a genuine cutoff constant to the inward primitive makes the boundary datum nonnegative globally and exactly dist²/2 on the working ball.

  1. def OAI.RegularPointCoordinates.positiveSquaredDistance line 21
  2. def OAI.RegularPointCoordinates.positiveSquaredDistanceValue line 25
  3. theorem OAI.RegularPointCoordinates.positiveSquaredDistance_representative line 29
  4. theorem OAI.RegularPointCoordinates.positiveSquaredDistanceValue_on_ball line 43
  5. theorem OAI.RegularPointCoordinates.positiveSquaredDistanceValue_bounds line 52
  6. theorem OAI.RegularPointCoordinates.positiveSquaredDistanceValue_lipschitz line 69
  7. theorem OAI.RegularPointCoordinates.positiveSquaredDistance_gamma line 108

    Source documentation

    The cutoff constant has zero local gradient. The exact distance chain rule is retained against every Sobolev test direction.

    theorem positiveSquaredDistance_gamma {p : X} {R C : ℝ} (hR : 0 ≤ R)
    (χ : GoodLaplacianCutoff μ hQ p R C) (a : SobolevSpace μ hQ) :
    ∀ᵐ x ∂μ.restrict (ball p R),
      localGamma μ hQ (positiveSquaredDistance μ hQ hR χ) a x =
        -dist p x * localGamma μ hQ (inwardSobolev μ hQ p R) a x := by
…

    Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.positiveSquaredDistance, OAI.RegularPointCoordinates.inwardSobolev

  8. theorem OAI.RegularPointCoordinates.positiveSquaredDistance_gradient line 142