OAI/Geometry/RCD/Sobolev/BochnerWeakSubsolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.weak_subsolution line 21

   Source documentation

   Positivity of the full Bochner measure, including any singular part, gives the distributional inequality for its Sobolev energy density.

   theorem LocalHarmonicEnergy.weak_subsolution
       {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
       {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
       (G : LocalHarmonicEnergy μ hQ U M κ p r L v) :
       IsWeakSubsolutionOn μ hQ (ball p (2*r)) G.energy (2*κ) := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.IsWeakSubsolutionOn