GridCollisions.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite terminal flags from actual independent grid shifts

For two different coordinate labels, their lattice-hit events have product probability. Countably many flagged points and finitely many label pairs can therefore be counted by Tonelli. Square-summable band widths imply a finite expected collision count, hence only finitely many flagged collisions for almost every choice of the grids.

def OAI.CircleDomainRigidity.FiniteTransfer.pairedLatticeIncidence line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.measurableSet_pairedLatticeIncidence line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.measure_pairedLatticeIncidence_le line 32
def OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount line 46

theorem OAI.CircleDomainRigidity.FiniteTransfer.lintegral_gridCollisionCount_le line 55

Source documentation

Exact pair laws and Tonelli yield the expected collision bound.

theorem lintegral_gridCollisionCount_le {n : ℕ} {P S : Type*}
    [Fintype P] [Countable S] {h : ℝ} (hh : 0 < h)
    (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
    (a b : Fin n → S → ℝ) :
    (∫⁻ θ, gridCollisionCount h pairs a b θ
      ∂Measure.pi (fun _ : Fin n => shiftLaw h)) ≤
      ∑ p, ∑' s, ENNReal.ofReal (min 1 ((b (pairs p).1 s - a (pairs p).1 s) / h)) *
        ENNReal.ofReal (min 1 ((b (pairs p).2 s - a (pairs p).2 s) / h)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount, OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw

theorem OAI.CircleDomainRigidity.FiniteTransfer.summable_grid_pair_probabilities line 74

Source documentation

The product majorant for two square-summable band widths is summable at every positive grid spacing.

theorem summable_grid_pair_probabilities {S : Type*} {h : ℝ} (hh : 0 < h)
    (a b : S → ℝ) (ha : ∀ s, 0 ≤ a s) (hb : ∀ s, 0 ≤ b s)
    (ha2 : Summable (fun s => a s ^ 2)) (hb2 : Summable (fun s => b s ^ 2)) :
    Summable (fun s => min 1 (a s / h) * min 1 (b s / h)) := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.tsum_grid_pair_probabilities_lt_top line 89

theorem OAI.CircleDomainRigidity.FiniteTransfer.lintegral_gridCollisionCount_lt_top line 109

Source documentation

Square-summable band widths make the actual expected collision count finite, rather than merely a formal upper bound.

theorem lintegral_gridCollisionCount_lt_top {n : ℕ} {P S : Type*}
    [Fintype P] [Countable S] {h : ℝ} (hh : 0 < h)
    (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
    (a b : Fin n → S → ℝ)
    (hwidth : ∀ i s, 0 ≤ b i s - a i s)
    (hwidth2 : ∀ i, Summable (fun s => (b i s - a i s) ^ 2)) :
    (∫⁻ θ, gridCollisionCount h pairs a b θ
      ∂Measure.pi (fun _ : Fin n => shiftLaw h)) < ∞ := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount, OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw

theorem OAI.CircleDomainRigidity.FiniteTransfer.ae_finite_grid_collision_flags line 129

Source documentation

A finite expected collision count has only finitely many active pair/flag incidences almost surely. Thus its projection onto flagged points is finite as well.

theorem ae_finite_grid_collision_flags {n : ℕ} {P S : Type*}
    [Fintype P] [Countable S] {h : ℝ} (hh : 0 < h)
    (pairs : P → Fin n × Fin n) (a b : Fin n → S → ℝ)
    (hfinite : (∫⁻ θ, gridCollisionCount h pairs a b θ
      ∂Measure.pi (fun _ : Fin n => shiftLaw h)) < ∞) :
    ∀ᵐ θ ∂Measure.pi (fun _ : Fin n => shiftLaw h),
      {s | ∃ p, θ ∈ pairedLatticeIncidence h (a (pairs p).1 s) (b (pairs p).1 s)
        (a (pairs p).2 s) (b (pairs p).2 s) (pairs p).1 (pairs p).2}.Finite := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount, OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw, OAI.CircleDomainRigidity.FiniteTransfer.pairedLatticeIncidence