OAI/Geometry/RCD/Coordinates/NormalizedPoissonEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_poisson_source_estimates line 19

   Source documentation

   The normalized Sobolev inequality yields a linear gradient error, a mass-times-height energy error, and the corresponding energy-density error.

   theorem normalized_poisson_source_estimates (Ω : Set X) (hΩ : MeasurableSet Ω)
       (hfin : μ Ω ≠ ∞) (hvol : 0 < μ.real Ω) {P : ℝ} (hP : 0 ≤ P)
       (hpoin : ∀ v : SobolevSpace.dirichlet μ hQ Ω,
         ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val)
       (q f : SobolevSpace μ hQ) (Q : X → ℝ) {L : ℝ≥0}
       (hQlip : LipschitzWith L Q) (hQ0 : ∀ x, 0 ≤ Q x)
       (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ] Q)
       {a B K A d C s : ℝ} (ha : 0 ≤ a) (hB : 0 ≤ B) (hK : 0 ≤ K)
       (hA : 0 ≤ A) (hd : 1 < d) (hC : 0 < C) (hs : 0 < s)
       (hQB : ∀ᵐ x ∂μ.restrict Ω, Q x ≤ B)
       (hgradq : ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.minimalSlope μ hQ q x ≤ A)
       (τ : SobolevSpace.dirichlet μ hQ Ω)
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope