GridCollisionEstimate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Vanishing scaled expectation for the actual collision count

The probability estimates are multiplied by the square of the grid spacing. This turns the normalized band probabilities into the clipped products min h a * min h b, dominated by summable oscillation products. Thus the actual random count, with its spacing-dependent law, satisfies the small-expectation premise of the reciprocal-grid selection theorem.

theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_pair_probability_eq line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_lintegral_gridCollisionCount_le line 30

theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_integral_gridCollisionCount_le line 79

Source documentation

The actual count is integrable, and its ordinary expected value satisfies the paper's scaled clipped-product estimate.

theorem scaled_integral_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 → ℝ)
    (hwidth : ∀ i s, 0 ≤ b i s - a i s)
    (hwidth2 : ∀ i, Summable (fun s => (b i s - a i s) ^ 2)) :
    Integrable (fun θ => (gridCollisionCount h pairs a b θ).toReal)
      (Measure.pi (fun _ : Fin n => shiftLaw h)) ∧
    h ^ 2 * (∫ θ, (gridCollisionCount h pairs a b θ).toReal
      ∂Measure.pi (fun _ : Fin n => shiftLaw h)) ≤
      ∑ p, ∑' s, min h (b (pairs p).1 s - a (pairs p).1 s) *
        min h (b (pairs p).2 s - a (pairs p).2 s) := by
…

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

theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_gridCollisionCount_mean_tendsto_zero line 108

Source documentation

The scaled collision expectation tends to zero along the exact reciprocal-integer grids and their actual independent shift laws.

theorem scaled_gridCollisionCount_mean_tendsto_zero {n : ℕ} {P S : Type*}
    [Fintype P] [Countable S]
    (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)) :
    Tendsto (fun N => reciprocalGridStep N ^ 2 *
      (∫ θ, (gridCollisionCount (reciprocalGridStep N) pairs a b θ).toReal
        ∂reciprocalGridLaw n N)) atTop (𝓝 0) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep, OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw