QuadraticGramError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Gram control of the quadratic model's energy error

theorem OAI.RegularPointCoordinates.quadratic_gram_error line 13

theorem OAI.RegularPointCoordinates.coordinateQuadratic_energy_error line 46

Source documentation

Near-orthonormal coordinate gradients make the energy density of the actual quadratic model close to twice its value.

theorem coordinateQuadratic_energy_error {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0)
    (hu : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C) :
    ∀ᵐ x ∂μ,
      |localGamma μ hQ (coordinateQuadratic μ hQ u C) (coordinateQuadratic μ hQ u C) x -
        2 * SobolevSpace.toLp μ hQ (coordinateQuadratic μ hQ u C) x| ≤
      (C : ℝ) ^ 2 * ∑ i, ∑ j, |localGamma μ hQ (u j) (u i) x - if j = i then 1 else 0| := by
…

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