GridIncidence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual probabilities that a shifted lattice meets a band

A grid of spacing h meets [a,b] exactly when the shift modulo h lies in the projection of this interval. Haar measure of that projection is at most min h (b-a). Under the actual normalized interval law for the shift, the probability is at most min 1 ((b-a)/h).

def OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence line 20
theorem OAI.CircleDomainRigidity.FiniteTransfer.addCircle_eq_iff_exists_int line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence_eq_preimage line 29
theorem OAI.CircleDomainRigidity.FiniteTransfer.measurableSet_latticeBandIncidence line 41
theorem OAI.CircleDomainRigidity.FiniteTransfer.volume_addCircle_interval_le line 48
theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw_latticeBandIncidence_eq line 65
Source documentation
The normalized interval shift law gives the exact quotient measure of the event, divided by the grid spacing.
```
theorem shiftLaw_latticeBandIncidence_eq {h : ℝ} [Fact (0 < h)] (a b : ℝ) :
    shiftLaw h (latticeBandIncidence h a b) =
      volume (((↑) : ℝ → AddCircle h) '' Icc a b) / ENNReal.ofReal h := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw, OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence
theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw_latticeBandIncidence_le line 81
Source documentation
The quantitative band-hit estimate used in the terminal-count expectation. It is proved for the actual normalized shift measure.
```
theorem shiftLaw_latticeBandIncidence_le {h : ℝ} (hh : 0 < h) (a b : ℝ) :
    shiftLaw h (latticeBandIncidence h a b) ≤
      ENNReal.ofReal (min 1 ((b - a) / h)) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw, OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence