OAI/Geometry/RCD/Sobolev/QuadraticValueGradientBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.cutoff_error_algebra line 13
2. theorem OAI.RegularPointCoordinates.coordinateQuadratic_value_gradient_bound line 41

   Source documentation

   The exact distance eikonal identity and the harmonic quadratic model bound the local gradient error by its value error and the Gram error. The constants B and T bound the actual trace and cutoff cross gradient.

   theorem coordinateQuadratic_value_gradient_bound {n : ℕ} {Ω : Set X}
       (hfin : μ Ω ≠ ∞)
       (u : Fin n → SobolevSpace μ hQ) (C D L : ℝ≥0)
       (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
       (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
       (c q : SobolevSpace μ hQ) (χ : X → ℝ)
       (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
       (hbound : ∀ x, |χ x| ≤ 1) (hnonneg : ∀ x, 0 ≤ χ x)
       (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
       (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤ D)
       {δ B T : ℝ} (hδ : 0 ≤ δ)
       (hsmall : ∀ᵐ x ∂μ.restrict Ω,
   …

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