PoissonGradientBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Interior gradient control from the proved Poisson height estimate

theorem OAI.RegularPointCoordinates.replacement_value_bound_of_height line 19

Source documentation

The nonnegative replacement defect and a bound on the boundary datum bound the absolute value of the actual Poisson replacement.

theorem replacement_value_bound_of_height (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    (q f : SobolevSpace μ hQ) (Ω : Set X) {B H : ℝ} (hBH : B ≤ H)
    (hq : ∀ᵐ x ∂μ.restrict Ω,
      0 ≤ SobolevSpace.toLp μ hQ q x ∧ SobolevSpace.toLp μ hQ q x ≤ B)
    (hh : ∀ᵐ x ∂μ.restrict Ω,
      0 ≤ SobolevSpace.toLp μ hQ (q - f) x ∧ SobolevSpace.toLp μ hQ (q - f) x ≤ H) :
    ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ f x| ≤ H := by
…

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

theorem OAI.RegularPointCoordinates.LocalPoissonGradientInput.bound_of_replacement line 35

Source documentation

The gradient input now applies to the constructed replacement: the required supremum bound is derived from the nonnegative Poisson defect.

theorem LocalPoissonGradientInput.bound_of_replacement {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} (hgradient : LocalPoissonGradientInput hX)
    (hn : 2 ≤ n)
    (p : X) {r c B H : ℝ} (hr : 0 < r) (hcurv : -1 ≤ K * r ^ 2)
    (hH : 0 ≤ H) (hBH : B ≤ H)
    (q f : SobolevSpace (hausdorff n X) hX.quadratic)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8 * r)) f c)
    (hq : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * r)),
      0 ≤ SobolevSpace.toLp (hausdorff n X) hX.quadratic q x ∧
        SobolevSpace.toLp (hausdorff n X) hX.quadratic q x ≤ B)
    (hh : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * r)),
      0 ≤ SobolevSpace.toLp (hausdorff n X) hX.quadratic (q - f) x ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonGradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp