OAI/Geometry/RCD/Coordinates/RestrictedCommutatorFit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_commutator_restrict line 19

   Source documentation

   The chosen fits only need to represent the radial derivatives on the smaller common ball. Restriction loses precisely the given volume ratio.

   theorem normalized_commutator_restrict {Ω Ω' : Set X}
       (hsub : Ω' ⊆ Ω) (hpos : 0 < μ.real Ω) (hpos' : 0 < μ.real Ω')
       (f v u g₀ h₀ g h : SobolevSpace μ hQ) {Cf Cv C E : ℝ}
       (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ Cf)
       (hv : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ v v x ≤ Cv)
       (hg₀ : SobolevSpace.toLp μ hQ g₀ =ᵐ[μ.restrict Ω] localGamma μ hQ f u)
       (hh₀ : SobolevSpace.toLp μ hQ h₀ =ᵐ[μ.restrict Ω] localGamma μ hQ v u)
       (hg : SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict Ω'] localGamma μ hQ f u)
       (hh : SobolevSpace.toLp μ hQ h =ᵐ[μ.restrict Ω'] localGamma μ hQ v u)
       (hE : 0 ≤ E) (hvol : μ.real Ω ≤ C * μ.real Ω')
       (he : (μ.real Ω)⁻¹ * (∫ x in Ω,
         (localGamma μ hQ v g₀ x - localGamma μ hQ f h₀ x - localGamma μ hQ v u x) ^ 2 ∂μ) ≤ E) :
   …

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