CompletionCounts.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The literal zero-penalty sum counts residual completions

Finite balanced large-cell assignments are represented by bounded natural matrices supported on the large cells. The zero-penalty predicate is equivalent to the actual padded residual table equations. An explicit entry bound proves when the formal capacities exclude no completion.

def OAI.ContingencyTables.CompletionCounts.LargeCompletion line 21
instance OAI.ContingencyTables.CompletionCounts.largeCompletionFintype line 24
def OAI.ContingencyTables.CompletionCounts.Assignment line 29
instance OAI.ContingencyTables.CompletionCounts.assignmentFintype line 32
def OAI.ContingencyTables.CompletionCounts.assignmentMatrix line 37
lemma OAI.ContingencyTables.CompletionCounts.assignment_supported line 41
lemma OAI.ContingencyTables.CompletionCounts.assignment_bounded line 45
def OAI.ContingencyTables.CompletionCounts.fullPenalty line 48
def OAI.ContingencyTables.CompletionCounts.ZeroAssignments line 54
instance OAI.ContingencyTables.CompletionCounts.zeroAssignmentsFintype line 58

theorem OAI.ContingencyTables.CompletionCounts.padded_total_le line 65

Source documentation

The total padded residual mass is at most the original mass plus one padding unit L for each large cell.

theorem padded_total_le (small : I → J → Bool) (X : I → J → ℕ) (r : I → ℕ) (L : ℕ) :
    (∑ i, (r i-smallRow small X i+rowLargeCount small i*L)) ≤
      (∑ i, r i)+(∑ i, rowLargeCount small i)*L := by
…

theorem OAI.ContingencyTables.CompletionCounts.capacity_excludes_none line 73

Source documentation

This is the exact reason the paper's formal large capacity excludes no padded completion. No large-range enumeration is used.

theorem capacity_excludes_none (small : I → J → Bool) (B X : I → J → ℕ)
    (r : I → ℕ) (L d C : ℕ) (hcount : (∑ i, rowLargeCount small i) ≤ d)
    (hC : (∑ i, r i)+d*L ≤ C) (hB : ∀ i j, small i j=false → B i j=C) :
    ∀ i j, small i j=false →
      (∑ k, (r k-smallRow small X k+rowLargeCount small k*L)) ≤ B i j := by
…

theorem OAI.ContingencyTables.CompletionCounts.large_count_le_dimension line 83
def OAI.ContingencyTables.CompletionCounts.paperCapacity line 98

theorem OAI.ContingencyTables.CompletionCounts.paper_capacity_excludes_none line 103

Source documentation

For the manuscript's exact C=N+dL+U+2, the capacity hypothesis of the count equivalence follows just from the dimension allowance.

theorem paper_capacity_excludes_none (small : I → J → Bool) (X : I → J → ℕ)
    (r : I → ℕ) (d L U : ℕ) (hd : Fintype.card I*Fintype.card J ≤ d) :
    ∀ i j, small i j=false →
      (∑ k, (r k-smallRow small X k+rowLargeCount small k*L)) ≤ paperCapacity small r d L U i j := by
…

Mentions: OAI.ContingencyTables.CompletionCounts.paperCapacity

def OAI.ContingencyTables.CompletionCounts.firstPaperSmall line 113
lemma OAI.ContingencyTables.CompletionCounts.firstPaperSmall_false_iff line 118
Source documentation
Thus the large set is exactly the complete large-margin rectangle.
```
lemma firstPaperSmall_false_iff (r : I → ℕ) (c : J → ℕ) (U : ℕ) (i : I) (j : J) :
    firstPaperSmall r c U i j=false ↔ U ≤ r i ∧ U ≤ c j := by
…
```
Mentions: OAI.ContingencyTables.CompletionCounts.firstPaperSmall
def OAI.ContingencyTables.CompletionCounts.dimensionAllowance line 122
lemma OAI.ContingencyTables.CompletionCounts.dimension_le_allowance line 125
def OAI.ContingencyTables.CompletionCounts.completionEquiv line 129

theorem OAI.ContingencyTables.CompletionCounts.hard_count_eq line 167

Source documentation

The finite hard marginal is exactly the padded completion count; if an original residual is negative every zero-penalty term vanishes.

theorem hard_count_eq (small : I → J → Bool) (B X Y : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ)
    (hX : ∀ i j, small i j=true → X i j ≤ B i j)
    (hY : ∀ i j, small i j=true → Y i j ≤ B i j)
    (hB : ∀ i j, small i j=false → (∑ k, (r k-smallRow small X k+rowLargeCount small k*L)) ≤ B i j) :
    (∑ a : Assignment small B, if fullPenalty small B X Y (assignmentMatrix a) r c L=0 then (1:ℝ) else 0) =
      if OriginalResidualsNonnegative small B X Y r c then
        (Fintype.card (LargeCompletion small (fun i => r i-smallRow small X i+rowLargeCount small i*L)
          (fun j => c j-smallColumn small B Y j+columnLargeCount small j*L)):ℝ) else 0 := by
…

Mentions: OAI.ContingencyTables.CompletionCounts.Assignment, OAI.ContingencyTables.CompletionCounts.fullPenalty, OAI.ContingencyTables.CompletionCounts.assignmentMatrix, OAI.ContingencyTables.CompletionCounts.LargeCompletion

def OAI.ContingencyTables.CompletionCounts.firstPaperWeight line 196
Source documentation
The first manuscript's actual supported padded-completion weight, with its dimension allowance, padding, threshold and formal capacity.
```
noncomputable def firstPaperWeight (r : I → ℕ) (c : J → ℕ) (X Y : I → J → ℕ) : ℝ :=
…
```
def OAI.ContingencyTables.CompletionCounts.firstPaperHardSum line 206
theorem OAI.ContingencyTables.CompletionCounts.firstPaperHardSum_eq_weight line 216
Source documentation
This identifies the actual finite zero-penalty large-assignment sum with the original supported completion count, on every small profile.
```
theorem firstPaperHardSum_eq_weight (r : I → ℕ) (c : J → ℕ) (X Y : I → J → ℕ)
    (hX : ∀ i j, firstPaperSmall r c (dimensionAllowance (I := I) (J := J)^20) i j=true →
…
```
Mentions: OAI.ContingencyTables.CompletionCounts.firstPaperSmall, OAI.ContingencyTables.CompletionCounts.dimensionAllowance