ActualSharpProjection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sharp projection for the actual two-center Poisson targets

theorem OAI.RegularPointCoordinates.exists_actual_projection_family line 19

Source documentation

Construct the compactness family from actual sources and replacements. No residual, forcing, or outer estimate is assumed in the configuration.

theorem exists_actual_projection_family {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 M : ℝ}
    (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) :
    ∃ family : SharpProjectionFamily hX
      (ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M) (1 / 1024) (1 / 2048),
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SharpProjectionFamily, OAI.RegularPointCoordinates.ActualProjectionConfiguration

theorem OAI.RegularPointCoordinates.actual_sharp_projection line 228

Source documentation

One sharp estimate for every actual two-center target satisfying the preceding geometric estimates. The only compactness input is the precise published Poisson/harmonic convergence theorem.

theorem actual_sharp_projection {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX) (hn : 2 ≤ n)
    {κ B J C A Cχ epsilon H D L M : ℝ}
    (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) :
    ∃ P : ℝ, 0 < P ∧ ∃ delta : ℝ, 0 < delta ∧
…

theorem OAI.RegularPointCoordinates.actual_sharp_projection_gradient line 252

Source documentation

The same sharp estimate controls the actual harmonic residual gradient on the smaller testing ball, in physical radius units.

theorem actual_sharp_projection_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX) (hn : 2 ≤ n)
    {κ B J C A Cχ epsilon H D L M : ℝ}
    (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) :
    ∃ Q : ℝ, 0 < Q ∧ ∃ delta : ℝ, 0 < delta ∧
…