OAI/Combinatorics/ContingencyTables/Dense/GridCover.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite cut-face cover of the interpolation shell

The continuous shell in the conductance argument is covered, except for the null grid hyperplanes, by the finite collection of interior cut-face tubes. No exterior faces or segment general-position hypotheses occur.

  1. abbrev OAI.ContingencyTables.GridBoundary.Grid line 23
  2. def OAI.ContingencyTables.GridBoundary.corner line 25
  3. def OAI.ContingencyTables.GridBoundary.mixGrid line 27
  4. theorem OAI.ContingencyTables.GridBoundary.corner_mix line 31
  5. def OAI.ContingencyTables.GridBoundary.Cube line 36
  6. def OAI.ContingencyTables.GridBoundary.selectedBins line 38
  7. def OAI.ContingencyTables.GridBoundary.IsGridEdge line 41
  8. abbrev OAI.ContingencyTables.GridBoundary.CutEdge line 45
  9. instance OAI.ContingencyTables.GridBoundary.(instance at line 49) line 49
  10. def OAI.ContingencyTables.GridBoundary.edgeTube line 52
  11. theorem OAI.ContingencyTables.GridBoundary.openBin_in_cube line 56
  12. theorem OAI.ContingencyTables.GridBoundary.near_finite_cut_tube line 63
  13. theorem OAI.ContingencyTables.GridBoundary.floor_grid line 95
  14. theorem OAI.ContingencyTables.GridBoundary.interpolation_short line 104
  15. theorem OAI.ContingencyTables.GridBoundary.interpolation_shell_cover line 125

    Source documentation

    Every shell point off the grid hyperplanes belongs to an interior cut-face tube. This is the actual cover used by the manuscript.

    theorem interpolation_shell_cover {q K : ℕ} (P : (Fin q → ℤ) → Prop)
    (t : ℝ) (ht : 0 < t) (ht₁ : t < 1) (hr : t * K ≤ 1)
    (z : Fin q → ℝ)
    (hz : z ∈ PublishedInputs.interpolate t (selectedBins K P) {y | Cube K y} \
      selectedBins K P)
    (hoff : ∀ j (k : ℤ), z j ≠ (k : ℝ)) :
    ∃ e : CutEdge K P, z ∈ edgeTube e (t * K) := by
…

    Mentions: OAI.ContingencyTables.PublishedInputs.interpolate, OAI.ContingencyTables.GridBoundary.selectedBins, OAI.ContingencyTables.GridBoundary.Cube, OAI.ContingencyTables.GridBoundary.CutEdge, OAI.ContingencyTables.GridBoundary.edgeTube

  16. theorem OAI.ContingencyTables.GridBoundary.ae_off_grid line 148

    Source documentation

    The only excluded points lie on countably many null hyperplanes.

    theorem ae_off_grid : ∀ᵐ z : I → ℝ ∂volume, ∀ j (k : ℤ), z j ≠ (k : ℝ) := by
…
  17. theorem OAI.ContingencyTables.GridBoundary.interpolation_shell_cover_ae line 156