NormalizedTransportDefect.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual transport error in the normalized source units

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.normalized_transport_defect line 21

Source documentation

At the fixed projection radius, the full Poisson defect supplies exactly the radial error budget required by normalized transport.

theorem DyadicDistanceReplacements.normalized_transport_defect
    {n : ℕ} {κ r0 B J C σ : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (hκ : 0 ≤ κ) (hB : 0 ≤ B)
    (hbudget : normalizedPoissonDefect μ hQ S i ≤ σ ^ 2)
    (hvol : |μ.real (ball p (distanceSourceRadius r0 i / 2048)) /
      (euclideanUnitVolume n * (distanceSourceRadius r0 i / 2048) ^ n) - 1| ≤ 1 / 4) :
    let R := distanceSourceRadius r0 i / 2048
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedPoissonDefect, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.euclideanUnitVolume