GridBoundary.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cut faces of a unit grid

The geometric step in the dense sampler's conductance proof: two points in differently labelled open bins at sup distance less than r ≤ 1 are within r of a common closed face of oppositely labelled axis neighbours. A coordinate path avoids any general-position assumption at simultaneous grid crossings.

def OAI.ContingencyTables.GridBoundary.mixed line 24
theorem OAI.ContingencyTables.GridBoundary.cut_edge_aux line 27
theorem OAI.ContingencyTables.GridBoundary.cut_edge line 44
Source documentation
A change of labels along a coordinate path occurs on an axis edge.
```
theorem cut_edge [Fintype I] (P : (I → ℤ) → Prop) (a b : I → ℤ)
    (ha : P a) (hb : ¬ P b) :
    ∃ S i, i ∉ S ∧ P (mixed a b S) ∧ ¬ P (mixed a b (insert i S)) := by
…
```
Mentions: OAI.ContingencyTables.GridBoundary.mixed
def OAI.ContingencyTables.GridBoundary.OpenBin line 52
def OAI.ContingencyTables.GridBoundary.ClosedBin line 55
theorem OAI.ContingencyTables.GridBoundary.short_bin_indices line 58
theorem OAI.ContingencyTables.GridBoundary.clamp_near line 70
theorem OAI.ContingencyTables.GridBoundary.adjacent_boundary line 85

theorem OAI.ContingencyTables.GridBoundary.near_cut_face line 108

Source documentation

The terminal point of a short displacement lies near an actual cut face. The intermediate bins use only the two endpoint indices in each coordinate, so they stay inside any rectangular grid containing them.

theorem near_cut_face [Fintype I] (P : (I → ℤ) → Prop)
    (a b : I → ℤ) (x z : I → ℝ) (r : ℝ)
    (ha : OpenBin a x) (hb : OpenBin b z)
    (hd : ∀ i, |z i - x i| < r) (hr : r ≤ 1)
    (hPa : P a) (hPb : ¬ P b) :
    ∃ S i w, i ∉ S ∧ P (mixed a b S) ∧ ¬ P (mixed a b (insert i S)) ∧
      (b i = a i + 1 ∨ a i = b i + 1) ∧
      ClosedBin (mixed a b S) w ∧ ClosedBin (mixed a b (insert i S)) w ∧
      (∀ j, |z j - w j| < r) := by
…

Mentions: OAI.ContingencyTables.GridBoundary.OpenBin, OAI.ContingencyTables.GridBoundary.mixed, OAI.ContingencyTables.GridBoundary.ClosedBin