ActualPoissonQuadratic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative quadratic approximation by actual Poisson replacements

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.scaled_datum_representative line 19

Source documentation

The actual datum, after physical rescaling, represents half the squared distance on the quarter ball.

theorem DyadicDistanceReplacements.scaled_datum_representative
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ) :
    SobolevSpace.toLp μ hQ (((distanceSourceRadius r0 i) ^ 2)⁻¹ • T.distanceDatum μ hQ i) =ᵐ[
      μ.restrict (ball p ((1 / 4) * distanceSourceRadius r0 i))]
      fun x => dist p x ^ 2 / (2 * (distanceSourceRadius r0 i) ^ 2) := by
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.distanceSourceRadius

theorem OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation.mono_error line 45
Source documentation
A larger error bound preserves both the metric and normalized-measure parts of the same measured coordinate approximation.
```
theorem IsMeasuredEuclideanApproximation.mono_error {n : ℕ} {p : X}
    {r R ε δ : ℝ} {V : X → Euclidean n}
    (h : IsMeasuredEuclideanApproximation (hausdorff n X) n p r R ε V)
    (hεδ : ε ≤ δ) :
    IsMeasuredEuclideanApproximation (hausdorff n X) n p r R δ V :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation, OAI.RegularPointCoordinates.hausdorff

theorem OAI.RegularPointCoordinates.actual_poisson_quadratic_error line 57

Source documentation

This is the quantitative quadratic-error field needed by the uniform sharp-projection family, derived from the full source budget and metric approximation of the actual coordinate representatives.

theorem actual_poisson_quadratic_error {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    {κ r0 B J C omega eta ε : ℝ} {p : X}
    {S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0}
    (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
    (hκ : 0 ≤ κ) (hB : 0 ≤ B) (heta : 0 ≤ eta) (hε : 0 ≤ ε)
    (hr01 : r0 ≤ 1) (homega : 0 < omega)
    (hvol : ∀ r : ℝ, 0 < r → r ≤ r0 →
      |(hausdorff n X).real (ball p r) / (omega * r ^ n) - 1| ≤ 1 / 4)
    (hsum : Summable (normalizedPoissonDefect (hausdorff n X) hX.quadratic S))
    (hbudget : (∑' j, normalizedPoissonDefect (hausdorff n X) hX.quadratic S j) ≤ eta)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedPoissonDefect