OAI/Geometry/RCD/Sobolev/PoissonSpanLinearLift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The coordinate inclusion as a continuous linear map

  1. def OAI.RegularPointCoordinates.poissonCoordinateLiftLinear line 12
  2. theorem OAI.RegularPointCoordinates.poissonCoordinateLiftLinear_apply line 36
  3. theorem OAI.RegularPointCoordinates.poissonSpanMap_comp_lift line 42

    Source documentation

    The coordinate block of the actual joint span is exactly the original map.

    theorem poissonSpanMap_comp_lift (μ : MeasureTheory.Measure X) (hQ : QuadraticCheegerEnergy μ)
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (f : Fin 2 → SobolevSpace μ hQ) :
    (sobolevColumnMap μ hQ (poissonSpan μ hQ u f)).comp (poissonCoordinateLiftLinear n) =
      sobolevColumnMap μ hQ u := by
…

    Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.poissonSpan, OAI.RegularPointCoordinates.poissonCoordinateLiftLinear