LocalConstantRepresentative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded Sobolev representatives of constants on a fixed ball

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_constant_representative line 18

Source documentation

A compact regular plateau represents the local constant without requiring a globally square-integrable constant function.

theorem NoncollapsedRCD.local_constant_representative {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2≤n) (p : X) (R c : ℝ) :
    ∃ d : SobolevSpace (hausdorff n X) hX.quadratic,
      (∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic d x|≤‖c‖₊) ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic d
        =ᵐ[(hausdorff n X).restrict (ball p R)] fun _ => c := by
…

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