BalancedFamily.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

All finite balanced-pair eliminations

The coordinates are the retained small coordinates followed by the actual finite list of large-cell pairs. The recursion performs their finite balanced sums and proves the total-slice positivity and removal signature at every step.

def OAI.ContingencyTables.BalancedFamily.Coordinates line 22
instance OAI.ContingencyTables.BalancedFamily.coordinatesFintype line 26
instance OAI.ContingencyTables.BalancedFamily.coordinatesDecidableEq line 34
def OAI.ContingencyTables.BalancedFamily.bounds line 42
def OAI.ContingencyTables.BalancedFamily.eliminate line 46
theorem OAI.ContingencyTables.BalancedFamily.eliminate_slices line 55
Source documentation
Every actual large-cell pair has width at least two; eliminating all of them preserves precisely the required box-valid total slice.
```
theorem eliminate_slices (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (F : (Coordinates I Ms → ℕ) → ℝ)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M)
    (hpos : PositiveSlice F (bounds m Ms) (R+Ms.sum))
    (hsig : RemovalSlice F (bounds m Ms) (R+Ms.sum)) :
    PositiveSlice (eliminate Ms F) m R ∧ RemovalSlice (eliminate Ms F) m R := by
…
```
Mentions: OAI.ContingencyTables.BalancedFamily.Coordinates, OAI.ContingencyTables.BalancedFamily.bounds, OAI.ContingencyTables.BalancedFamily.eliminate
theorem OAI.ContingencyTables.BalancedFamily.eliminate_congr_slice line 74
Source documentation
Only the paper's finite box and required total slice are ever read by a balanced marginal. In particular its zero extension is harmless.
```
theorem eliminate_congr_slice (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (F f : (Coordinates I Ms → ℕ) → ℝ)
    (heq : ∀ x, InBox (bounds m Ms) x → (∑ i, x i)=R+Ms.sum → F x=f x)
    (z : I → ℕ) (hz : InBox m z) (htotal : (∑ i, z i)=R) :
    eliminate Ms F z=eliminate Ms f z := by
…
```
Mentions: OAI.ContingencyTables.BalancedFamily.Coordinates, OAI.ContingencyTables.BalancedFamily.bounds, OAI.ContingencyTables.BalancedFamily.eliminate
theorem OAI.ContingencyTables.BalancedFamily.eliminate_nonnegative line 93
theorem OAI.ContingencyTables.BalancedFamily.eliminate_reflect line 107
Source documentation
Reflection reverses the finite index in every summed large pair and also reflects every retained coordinate.
```
theorem eliminate_reflect (Ms : List ℕ) (m : I → ℕ)
    (F : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ) :
    eliminate Ms (fun x => F (IntegerReflection.reflect (bounds m Ms) x)) z =
      eliminate Ms F (IntegerReflection.reflect m z) := by
…
```
Mentions: OAI.ContingencyTables.BalancedFamily.Coordinates, OAI.ContingencyTables.BalancedFamily.eliminate, OAI.ContingencyTables.IntegerReflection.reflect, OAI.ContingencyTables.BalancedFamily.bounds

theorem OAI.ContingencyTables.BalancedFamily.eliminate_tendsto line 125

Source documentation

All balanced eliminations are finite sums, so their actual values commute with the equality-softening limit.

theorem eliminate_tendsto {K : Type*} {l : Filter K} (Ms : List ℕ)
    (F : K → (Coordinates I Ms → ℕ) → ℝ) (f : (Coordinates I Ms → ℕ) → ℝ)
    (hlim : ∀ z, Filter.Tendsto (fun t => F t z) l (nhds (f z))) (z : I → ℕ) :
    Filter.Tendsto (fun t => eliminate Ms (F t) z) l (nhds (eliminate Ms f z)) := by
…

Mentions: OAI.ContingencyTables.BalancedFamily.Coordinates, OAI.ContingencyTables.BalancedFamily.eliminate