Tiling.lean`

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Tiling.band line 16
Source documentation
The literal closed height bands. Adjacent bands share only their endpoint, where every clipping proposal retains the old field.
```
def band (a q : ℝ) (k : ℤ) : Set ℝ := Set.Icc (q+k*a) (q+(k+1)*a)
```
lemma OAI.PlanarL1.Tiling.band_closed line 18
lemma OAI.PlanarL1.Tiling.band_convex line 19
def OAI.PlanarL1.Tiling.index line 21
lemma OAI.PlanarL1.Tiling.mem_band_index line 23
lemma OAI.PlanarL1.Tiling.lower_le_upper line 31
lemma OAI.PlanarL1.Tiling.overlap line 34
def OAI.PlanarL1.Tiling.processed line 44
Source documentation
The finite list is precisely the closed bands meeting the prescribed closed height window, not a truncation at individual points of a band.
```
noncomputable def processed (a q L U : ℝ) : Finset ℤ :=
…
```
lemma OAI.PlanarL1.Tiling.mem_processed line 48
lemma OAI.PlanarL1.Tiling.processed_covers line 68
def OAI.PlanarL1.Tiling.NearBoundary line 74
Source documentation
Small-ball height loss is proximity to a genuine band boundary.
```
def NearBoundary (a q h t : ℝ) : Prop := ∃ k : ℤ, |h-(q+k*a)|≤t
```
lemma OAI.PlanarL1.Tiling.same_band_of_avoid line 76
lemma OAI.PlanarL1.FiniteRandom.integer_interval_count line 99
lemma OAI.PlanarL1.FiniteRandom.periodic_probability line 129
Source documentation
Uniformly shifting a periodic tiling has its true one-dimensional bound. The extra two grid points cover both endpoints, independently of the band index.
```
lemma periodic_probability (m : ℕ) (hm : 0 < m) {a t : ℝ} (ha : 0<a)
    (ht : 0≤t) (h : ℝ) :
    prob (fun i : Fin (m+1) => Tiling.NearBoundary a (a/m*i.val) h t) ≤
      (2*t+2*a/m)/a := by
…
```
Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Tiling.NearBoundary
def OAI.PlanarL1.Tiling.Padded line 204
Source documentation
Strict padding in the actual floor-indexed band.
```
def Padded (a q h t : ℝ) : Prop :=
…
```
lemma OAI.PlanarL1.Tiling.NearBoundary.mono line 207
lemma OAI.PlanarL1.Tiling.NearBoundary.perturb line 210
lemma OAI.PlanarL1.Tiling.padded_of_avoid line 218
lemma OAI.PlanarL1.Tiling.index_eq_of_mem_lt line 233
lemma OAI.PlanarL1.Tiling.same_index_of_avoid line 238
lemma OAI.PlanarL1.Tiling.padded_pair line 244
lemma OAI.PlanarL1.Tiling.band_subset_of_padding line 250
lemma OAI.PlanarL1.FiniteRandom.prob_or_le line 264
lemma OAI.PlanarL1.FiniteRandom.prob_compl line 271
lemma OAI.PlanarL1.FiniteRandom.prob_eval_bound line 276
lemma OAI.PlanarL1.Tiling.height_pair_probability line 291
Source documentation
The two endpoint height tests use one shift, so their failures are bounded by an enlarged interval, not by a union bound over the vertices or columns.
```
lemma height_pair_probability (m : ℕ) (hm : 10000 ≤ m) {a h x : ℝ} (ha : 0<a)
    (htrim : a₂≤a) (hd : |x-h|≤a₂/10000) :
    prob (fun i : Fin (m+1) => ¬(Padded a (a/m*i.val) h (a/10) ∧
      Padded a (a/m*i.val) x (a/10)))≤21/100 := by
…
```
Mentions: OAI.PlanarL1.Tiling.Padded
lemma OAI.PlanarL1.Tiling.narrow_contained line 312
lemma OAI.PlanarL1.Tiling.unique_band_of_padded line 324