SubsolutionL1Mean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local L¹ mean bounds for nonnegative weak subsolutions

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.subsolution_l1_mean_value line 18

Source documentation

Interior interpolation removes every dependence on the initially known upper bound. The final estimate only uses the normalized L¹ mass.

theorem NoncollapsedRCD.subsolution_l1_mean_value {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (Λ : ℝ) (hΛ : 0 ≤ Λ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
      ∀ (u : SobolevSpace (hausdorff n X) hX.quadratic) (a B : ℝ),
      0 ≤ a → a*R^2 ≤ Λ → 0 ≤ B →
      IsWeakSubsolutionOn (hausdorff n X) hX.quadratic (ball p R) u a →
      (∀ᵐ y ∂(hausdorff n X).restrict (ball p R),
        0 ≤ SobolevSpace.toLp _ _ u y ∧ SobolevSpace.toLp _ _ u y ≤ B) →
      ∀ᵐ y ∂(hausdorff n X).restrict (ball p (R/2)),
        SobolevSpace.toLp _ _ u y ≤ C*((hausdorff n X).real (ball p R))⁻¹*
          ∫ z in ball p R, SobolevSpace.toLp (hausdorff n X) hX.quadratic u z ∂hausdorff n X := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsWeakSubsolutionOn, OAI.RegularPointCoordinates.SobolevSpace.toLp