ActualTwoCenterProjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual two-center Poisson projection and its scalar forcing

theorem OAI.RegularPointCoordinates.actual_two_center_projection line 20

Source documentation

The projected function is constructed from the two actual Poisson replacements. Its scalar forcing is controlled by the original defects and the already constructed coordinate radial fits. The constant precedes all centers, root radii and dyadic indices.

theorem actual_two_center_projection {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    {κ B J C A Cχ epsilon H D : ℝ}
    (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hJ : 0 ≤ J)
    (hCχ : 0 ≤ Cχ) (hA : 0 ≤ A) (hepsilon : 0 ≤ epsilon)
    (hH : 0 ≤ H) (hD : 0 ≤ D) :
    ∃ F : ℝ, 0 ≤ F ∧ ∀ {r0 : ℝ} (p₁ p₂ z : X)
    (S₁ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₁ r0)
    (S₂ : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p₂ r0)
…

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