RegularPairEndpoints.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ambient pair separation at the scale selected by the iteration

theorem OAI.RegularPointCoordinates.source_eq_ellipsoidRadius line 13

theorem OAI.RegularPointCoordinates.RegularBilinearData.pair_endpoints_at_scale line 31

Source documentation

The precise approximation error is small relative to the original ambient pair distance at the chosen dyadic scale.

theorem pair_endpoints_at_scale {L : ℝ} (hL : 2097152 ≤ L)
    (hzeta : 0 ≤ zeta) (hzetaL : zeta * L ≤ 2097152)
    (i : ℕ) {q z : X} (hq : q ∈ ball base (d.radius / 32))
    (hlow : L * dist q z ≤ distanceSourceRadius d.radius (d.shift + i))
    (hupp : distanceSourceRadius d.radius (d.shift + i) ≤ 2 * L * dist q z) :
    (1 / 4 : ℝ) * dist q z ≤ ‖d.frozenAt q i (d.values z - d.values q)‖ ∧
    ‖d.frozenAt q i (d.values z - d.values q)‖ ≤ 4 * dist q z := by
…

Mentions: OAI.RegularPointCoordinates.distanceSourceRadius