OAI/Geometry/RCD/Sobolev/ActualPoissonEulerForcing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.actual_poisson_euler_forcing line 20

   Source documentation

   Poincare constructs the scalar error from the actual full-mass Euler-gradient estimate. The normalized squared error is linear in the original two source defects, with one constant at every dyadic scale.

   theorem actual_poisson_euler_forcing {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hhessian : LocalPoissonHessianActionInput hX)
       (hproduct : LocalPoissonGradientProductInput hX)
       (hpoincare : LocalMeanPoincareInput hX) {κ : ℝ} (hκ : 0 ≤ κ) :
       ∃ Cp : ℝ, 1 ≤ Cp ∧ ∀
       {B J C A Cχ epsilon r0 : ℝ} (_hK : -κ ≤ K)
       (_hB : 0 ≤ B) (_hJ : 0 ≤ J) (_hCχ : 0 ≤ Cχ)
       (_hA : 0 ≤ A) (_hepsilon : 0 ≤ epsilon) (p₁ p₂ z : X)
       (S₁ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₁ r0)
       (S₂ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₂ r0)
       (T₁ : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S₁ B J C)
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements