OAI/Geometry/RCD/Coordinates/RegularPinchingField.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One actual matrix and energy family for all finite patches

  1. structure OAI.RegularPointCoordinates.RegularPinchingField line 19

    Source documentation

    These are constructed from the original full Bochner measure and the actual Poisson sources. The common positive floor permits a fixed energy minimizer in each finite patch.

    structure RegularPinchingField {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [(hausdorff n X).Regular] {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta : ℝ} (d : RegularBilinearData hX base hk enlargement zeta)
    (C budget : ℝ) where
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularBilinearData

  2. theorem OAI.RegularPointCoordinates.exists_regular_pinching_field line 36