SuffixCollision.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The local collision estimate in the all-dimensional suffix step

A projection test on the entire second conditional cell controls every translated collision window. Quadratic distance linearization transfers that test to the original distance pushforward, before any cell grouping.

theorem OAI.Falconer.projection_shifted_band_bound line 19
theorem OAI.Falconer.affine_distance_collision line 42
theorem OAI.Falconer.local_distance_collision_bound line 57

theorem OAI.Falconer.suffix_cell_collision_bound line 84

Source documentation

The geometric hypotheses are supplied by the actual center separation and common child side, not by an abstract distance approximation.

theorem suffix_cell_collision_bound (μ ν : Measure (Space d))
    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (P Q : DyadicCube d) (hP : 0 < P.side) (hQ : Q.side = P.side)
    {g w : ℝ} (hg : 0 < g) (hsep : g ≤ ‖P.center-Q.center‖) (hw : 0 < w)
    (hsmall : 2*(d:ℝ)*P.side^2/g ≤ w) {H : ℝ≥0∞}
    (hproj : ((ν.restrict Q.carrier).prod (ν.restrict Q.carrier))
      {z : Space d × Space d |
        |inner ℝ (‖P.center-Q.center‖⁻¹ • (P.center-Q.center)) (z.1-z.2)| ≤ w} ≤ H) :
    (((μ.restrict P.carrier).prod (ν.restrict Q.carrier)).prod
      ((μ.restrict P.carrier).prod (ν.restrict Q.carrier)))
        {z | |dist z.1.1 z.1.2-dist z.2.1 z.2.2| ≤ w} ≤
      (μ P.carrier)^2 * (((PlanarFalconer.bandOffsets 3).card : ℝ≥0∞)*H) :=
…

Mentions: OAI.Falconer.Space, OAI.Falconer.DyadicCube, OAI.PlanarFalconer.bandOffsets