ForestCut.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Signed cut equations for the actual physical table views

Small row and column views may disagree. Their two incidences therefore remain separate in the cut formula. Large cells have a single physical value at both endpoints, so every internal large-cell contribution cancels.

def OAI.ContingencyTables.ForestCut.indicator line 20
lemma OAI.ContingencyTables.ForestCut.abs_indicator_sub line 23
def OAI.ContingencyTables.ForestCut.rowDifference line 26
def OAI.ContingencyTables.ForestCut.columnDifference line 29
def OAI.ContingencyTables.ForestCut.cutTerm line 32
theorem OAI.ContingencyTables.ForestCut.signed_cut_identity line 38
Source documentation
Literal signed summation of the nonroot margin differences.
```
theorem signed_cut_identity (small : I → J → Bool) (rowU : I → Bool) (colU : J → Bool)
    (x q z X : I → J → ℝ) :
    (∑ i, indicator (rowU i)*rowDifference small x z X i)-
      (∑ j, indicator (colU j)*columnDifference small q z X j) =
      ∑ i, ∑ j, cutTerm small rowU colU x q z X i j := by
…
```
Mentions: OAI.ContingencyTables.ForestCut.indicator, OAI.ContingencyTables.ForestCut.rowDifference, OAI.ContingencyTables.ForestCut.columnDifference, OAI.ContingencyTables.ForestCut.cutTerm
theorem OAI.ContingencyTables.ForestCut.cut_sum_zero line 57
Source documentation
When U avoids roots, all selected nonroot equations hold, giving the source's cut cancellation even on unbalanced small profiles.
```
theorem cut_sum_zero (small : I → J → Bool) (rowU : I → Bool) (colU : J → Bool)
    (x q z X : I → J → ℝ)
    (hr : ∀ i, rowU i=true → rowDifference small x z X i=0)
    (hc : ∀ j, colU j=true → columnDifference small q z X j=0) :
    (∑ i, ∑ j, cutTerm small rowU colU x q z X i j)=0 := by
…
```
Mentions: OAI.ContingencyTables.ForestCut.rowDifference, OAI.ContingencyTables.ForestCut.columnDifference, OAI.ContingencyTables.ForestCut.cutTerm
lemma OAI.ContingencyTables.ForestCut.small_term_bound line 76
lemma OAI.ContingencyTables.ForestCut.free_term_bound line 98

theorem OAI.ContingencyTables.ForestCut.displacement_bound line 117

Source documentation

Isolating the sole crossing tree edge in the actual signed cut equations gives the forest displacement bound. Small cells retain both incidences, so the statement covers every unbalanced small profile.

theorem displacement_bound (small tree : I → J → Bool)
    (rowU : I → Bool) (colU : J → Bool) (x q z X b : I → J → ℝ)
    (i₀ : I) (j₀ : J) (d : ℝ)
    (hd : (Fintype.card I*Fintype.card J : ℕ)≤d)
    (hB : 1≤b i₀ j₀) (hs₀ : small i₀ j₀=false)
    (hcross : rowU i₀≠colU j₀)
    (hr : ∀ i, rowU i=true → rowDifference small x z X i=0)
    (hc : ∀ j, colU j=true → columnDifference small q z X j=0)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
    (hsmall : ∀ i j, small i j=true →
      b i j≤b i₀ j₀ ∧ (0≤x i j ∧ x i j≤b i j) ∧ (0≤q i j ∧ q i j≤b i j))
    (htree : ∀ i j, tree i j=true → (i,j)≠(i₀,j₀) → rowU i=colU j)
…

Mentions: OAI.ContingencyTables.ForestCut.rowDifference, OAI.ContingencyTables.ForestCut.columnDifference

lemma OAI.ContingencyTables.ForestCut.physical_interval_of_displacement line 177
Source documentation
The interval bound needed in the equality-softening count argument follows from the proved cut displacement estimate, with ample slack.
```
lemma physical_interval_of_displacement (d b X z : ℝ) (hd : 1 ≤ d) (hb : 0 ≤ b)
    (hX : 0 ≤ X ∧ X ≤ b) (hz : |z-X| ≤ 4*d*b) :
    -10*d*b ≤ z ∧ z ≤ 10*d*b := by
…
```