HessianSpanCommutator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Poisson-span commutator with the original Bochner masses

theorem OAI.RegularPointCoordinates.LocalPoissonHessianActionInput.span_commutator_directional line 18

Source documentation

The Hessian action estimate yields the actual commutator error and keeps the full shifted and ordinary Bochner masses explicit.

theorem LocalPoissonHessianActionInput.span_commutator_directional
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalPoissonHessianActionInput hX)
    {κ : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (p : X) (r : ℝ) (hr : 0 < r) (L : ℝ≥0)
    (U : Euclidean (n + 2) →L[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (ell : Euclidean (n + 2) →ₗ[ℝ] ℝ)
    (hU : ∀ v, IsConstantLaplacianOn (hausdorff n X) hX.quadratic
      (ball p (8 * r)) (U v) (ell v))
    (hgrad : ∀ v, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * r)),
      localGamma (hausdorff n X) hX.quadratic (U v) (U v) x ≤ (L : ℝ) ^ 2 * ‖v‖ ^ 2) :
    ∃ M : PositiveBilinearMeasure X (Euclidean (n + 2)),
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.PositiveBilinearMeasure

theorem OAI.RegularPointCoordinates.LocalPoissonHessianActionInput.span_commutator line 65

Source documentation

The uniform span bound follows by using its common gradient constant.

theorem LocalPoissonHessianActionInput.span_commutator
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalPoissonHessianActionInput hX)
    {κ : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (p : X) (r : ℝ) (hr : 0 < r) (L : ℝ≥0)
    (U : Euclidean (n + 2) →L[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (ell : Euclidean (n + 2) →ₗ[ℝ] ℝ)
    (hU : ∀ v, IsConstantLaplacianOn (hausdorff n X) hX.quadratic
      (ball p (8 * r)) (U v) (ell v))
    (hgrad : ∀ v, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * r)),
      localGamma (hausdorff n X) hX.quadratic (U v) (U v) x ≤ (L : ℝ) ^ 2 * ‖v‖ ^ 2) :
    ∃ M : PositiveBilinearMeasure X (Euclidean (n + 2)),
…