OAI/Geometry/RCD/Coordinates/QuadraticCoordinateGradient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual gradient of the quadratic coordinate model

  1. theorem OAI.RegularPointCoordinates.half_square_gamma line 16
  2. theorem OAI.RegularPointCoordinates.finite_half_square_gamma line 25
  3. theorem OAI.RegularPointCoordinates.coordinateQuadratic_gradient line 44
  4. theorem OAI.RegularPointCoordinates.coordinateQuadratic_gradient_self line 53

    Source documentation

    The quadratic model has the expected energy density, with the actual coordinate Gram entries. No Euclidean identity for that Gram is assumed.

    theorem coordinateQuadratic_gradient_self {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (C : ℝ≥0) (hu : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C) :
    localGamma μ hQ (coordinateQuadratic μ hQ u C) (coordinateQuadratic μ hQ u C) =ᵐ[μ]
      fun x => ∑ i, ∑ j, (SobolevSpace.toLp μ hQ (u i) x * SobolevSpace.toLp μ hQ (u j) x) *
        localGamma μ hQ (u j) (u i) x := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.coordinateQuadratic