RadialValueVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Averaging the transferred Poisson radial values

theorem OAI.RegularPointCoordinates.radial_fit_value_volume_units line 11

Source documentation

A source-to-volume ratio and the same scalar fit bound control the Poisson value error in the radial length unit.

theorem radial_fit_value_volume_units {r W M C B D w E Θ e : ℝ}
    (hW : 0 < W) (hC : 0 ≤ C) (hB : 0 ≤ B) (hE : 0 ≤ E)
    (hM : M / W ≤ Θ * E)
    (he : e ≤ 2 * (W * (D * r * w * Real.sqrt E) ^ 2) +
      2 * (C * w ^ 2) * (M * (B * (64 * r) ^ 2))) :
    W⁻¹ * e ≤ (2 * D ^ 2 + 8192 * C * B * Θ) * (r * w) ^ 2 * E := by
…