OAI/Geometry/RCD/Coordinates/RegularFiniteSpan.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Laplacian and Gram representatives of a regular finite span

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_finite_span line 21

    Source documentation

    Every finite family in the proved regular test core has a common linear Laplacian and a symmetric Sobolev Gram form.

    theorem NoncollapsedRCD.regular_finite_span {K : ℝ} {n m : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {Ω : Set X} (u : Fin m → compactLaplacianCore (hausdorff n X) hX.quadratic Ω) :
    let U := sobolevColumnMap (hausdorff n X) hX.quadratic (fun i => (u i).val)
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.sobolevColumnMap