OAI/Geometry/RCD/Harmonic/ContinuousAffineImprovement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform affine improvement for continuous local harmonic coordinates

  1. def OAI.RegularPointCoordinates.HasNormalizedAffineImprovement line 17

    Source documentation

    The normalized harmonic estimate in the original affine coordinate span.

    def HasNormalizedAffineImprovement {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (p : X) (r θ : ℝ) : Prop :=
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff

  2. theorem OAI.RegularPointCoordinates.affine_improvement_from_continuous_coordinates line 32