SuffixGrouping.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Coarse grouping of the actual all-dimensional distance cells

Two fine distance distributions sharing one bin force all distances of their full cell pairs into a common coarse collision band. The width constant retains the ambient dimension explicitly.

def OAI.Falconer.cellDistance line 18
instance OAI.Falconer.cellDistance_finite line 22
theorem OAI.Falconer.cellDistance_mass line 27
theorem OAI.Falconer.cellDistance_bin_witness line 32
theorem OAI.Falconer.cell_distance_variation line 45
theorem OAI.Falconer.shared_bin_full_cell_collision line 57

theorem OAI.Falconer.finite_suffix_cell_comparison line 109

Source documentation

The full suffix cell grouping. Local projection tests apply to the entire second conditional cell; the selected submeasure may be arbitrary.

theorem finite_suffix_cell_comparison {ι : Type*} (S : Finset ι)
    (μ ν : Measure (Space d)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (P Q : ι → DyadicCube d) (e : ι → Space d)
    (α : ι → Measure ℝ) [∀ i, IsFiniteMeasure (α i)]
    {s w : ℝ} (hs : 0 ≤ s) (hw : 0 < w) (hws : w ≤ s)
    (hP : ∀ i ∈ S, (P i).side = s) (hQ : ∀ i ∈ S, (Q i).side = s)
    (hα : ∀ i ∈ S, α i ≤ cellDistance μ ν (P i) (Q i))
    (haff : ∀ i ∈ S, ∀ x ∈ (P i).carrier, ∀ y ∈ (Q i).carrier,
      |dist x y-inner ℝ (e i) (x-y)| ≤ w)
    (F : ℝ≥0∞)
    (hproj : ∀ i ∈ S, ((ν.restrict (Q i).carrier).prod (ν.restrict (Q i).carrier))
      {z : Space d × Space d | |inner ℝ (e i) (z.1-z.2)| ≤ w} ≤
…

Mentions: OAI.Falconer.Space, OAI.Falconer.DyadicCube, OAI.Falconer.cellDistance