OAI/Geometry/RCD/Coordinates/GammaCoordinateForm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pointwise coordinate forms for pairs of Sobolev linear families

  1. theorem OAI.RegularPointCoordinates.localGamma_finset_sum_left line 16
  2. theorem OAI.RegularPointCoordinates.localGamma_finset_sum_right line 30
  3. def OAI.RegularPointCoordinates.gammaCoordinateForm line 46
  4. theorem OAI.RegularPointCoordinates.gammaCoordinateForm_rep line 53

    Source documentation

    Two different Sobolev linear families have one finite coordinate bilinear form, representing every fixed pair of gradient directions.

    theorem gammaCoordinateForm_rep (U V : Euclidean m →L[ℝ] SobolevSpace μ hQ)
    (a b : Euclidean m) :
    localGamma μ hQ (U a) (V b) =ᵐ[μ] fun x => gammaCoordinateForm μ hQ U V x a b := by
…

    Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.gammaCoordinateForm