ActualProjectionOuter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform outer estimates for the actual two-center Poisson projection

theorem OAI.RegularPointCoordinates.actual_two_center_projection_outer line 21

Source documentation

The same actual projection satisfies a uniform outer estimate. The transport error is constructed from the second Poisson replacement and its full source measure. All three constants precede the centers and scales.

theorem actual_two_center_projection_outer {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {κ B J C A Cχ epsilon H D L : ℝ}
    (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) (hL : 0 ≤ L) :
    ∃ F G₀ T₀ : ℝ, 0 ≤ F ∧ 0 ≤ G₀ ∧ 0 ≤ T₀ ∧ ∀ {r0 : ℝ} (p₁ p₂ : X)
    (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.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.DyadicDistanceSources