OAI/Geometry/RCD/Harmonic/QuadraticRadialError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.gram_action_sq line 13
2. theorem OAI.RegularPointCoordinates.coordinateQuadratic_raw_error line 50

   Source documentation

   Near-orthonormal coordinate gradients identify the gradient of the quadratic model with the corresponding coordinate values in L2. Together with the value-to-gradient estimate this proves the raw radial convergence.

   theorem coordinateQuadratic_raw_error {n : ℕ} {Ω : Set X} (hfin : μ Ω ≠ ∞)
       (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0) (q : SobolevSpace μ hQ)
       (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
       {M : ℝ} (hM : 0 ≤ M)
       (hgrad : ∀ j, ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ (u j) (u j) x ≤ M ^ 2)
       (j : Fin n) :
       let H := coordinateQuadratic μ hQ u C
   …

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