SubsolutionInterpolation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Interpolation of local subsolution mean bounds

theorem OAI.RegularPointCoordinates.IsWeakSubsolutionOn.mono line 19
Source documentation
Distributional subsolutions restrict to smaller test domains.
```
theorem IsWeakSubsolutionOn.mono (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    {s t : Set X} {u : SobolevSpace μ hQ} {a : ℝ}
    (hu : IsWeakSubsolutionOn μ hQ t u a) (hst : s ⊆ t) :
    IsWeakSubsolutionOn μ hQ s u a := by
…
```
Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakSubsolutionOn

theorem OAI.RegularPointCoordinates.sqrt_interpolation line 27

Source documentation

Young's inequality in the square-root form used for interior interpolation.

theorem sqrt_interpolation {θ c C H : ℝ} (hθ : 0 < θ) (hc : 0 ≤ c)
    (hC : 0 ≤ C) (hH : 0 ≤ H) :
    c*Real.sqrt (C*H) ≤ θ*C+(c^2/θ)*H := by
…

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_mean_interpolation line 45

Source documentation

A bound on a smaller ball interpolates the local L² norm with the L¹ mass on the fixed outer ball.

theorem NoncollapsedRCD.local_mean_interpolation {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) {p q : X} {R r D C : ℝ}
    (hR : 0 < R) (hr : 0 < r) (_hD : 0 ≤ D) (hC : 0 ≤ C)
    (hsub : ball q r ⊆ ball p R)
    (hvol : (hausdorff n X).real (ball p R) ≤ D*(hausdorff n X).real (ball q r))
    (u : SobolevSpace (hausdorff n X) hX.quadratic)
    (hpos : ∀ᵐ y ∂(hausdorff n X).restrict (ball p R), 0 ≤ SobolevSpace.toLp _ _ u y)
    (hbound : ∀ᵐ y ∂(hausdorff n X).restrict (ball q r), SobolevSpace.toLp _ _ u y ≤ C) :
    harmonicTargetNorm hX q r u ≤ Real.sqrt (D*C*
      ((hausdorff n X).real (ball p R))⁻¹*
        ∫ y in ball p R, SobolevSpace.toLp (hausdorff n X) hX.quadratic u y ∂hausdorff n X) := by
…

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