CompanionTerminalMass.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual terminal companion normalizer approximates the table count

abbrev OAI.ContingencyTables.CompanionTerminalMass.TreeCell line 16
structure OAI.ContingencyTables.CompanionTerminalMass.Endpoints line 21
Source documentation
These are the actual attained minima and maxima after the paper's integer bound-tightening step. They are feasible tables, not marginal mass or signature assumptions.
```
structure Endpoints (A : Instance I J) where
…
```
def OAI.ContingencyTables.CompanionTerminalMass.tableCount line 33
lemma OAI.ContingencyTables.CompanionTerminalMass.tableCount_ge_one line 36
lemma OAI.ContingencyTables.CompanionTerminalMass.treeCell_card_le line 48

lemma OAI.ContingencyTables.CompanionTerminalMass.total_near_mass_le line 54

Source documentation

Actual endpoint tables and the proved scalar signature estimates control the entire union of narrow tree violations.

lemma total_near_mass_le (A : Instance I J) (E : Endpoints A) (alpha gamma : ℝ)
    (ha : 0 ≤ alpha) (hg : 0 < gamma) (hW : 20*A.d ≤ A.W) (B K : ℕ)
    (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K) (hK : 0 < K) :
    (∑ t : TreeCell A,nearMass A alpha t.val gamma) ≤
      (4*A.d*gamma*K:ℝ)*physicalMass A alpha := by
…

Mentions: OAI.ContingencyTables.CompanionTerminalMass.Endpoints, OAI.ContingencyTables.CompanionTerminalMass.TreeCell

lemma OAI.ContingencyTables.CompanionTerminalMass.feasible_sum_eq_tableCount line 77
lemma OAI.ContingencyTables.CompanionTerminalMass.mass_le_table_far_near line 84

theorem OAI.ContingencyTables.CompanionTerminalMass.terminal_count_estimate line 115

Source documentation

This is the literal terminal normalizer estimate. The finite table bijection, root integrality, far bound and actual tree-marginal estimates are all proved. Arithmetic conditions below are discharged by the manuscript's explicit choices of K, gamma and the final coefficient.

theorem terminal_count_estimate (A : Instance I J) (E : Endpoints A)
    (alpha gamma epsilon : ℝ) (B K : ℕ)
    (ha : 0 < alpha) (hg : 0 < gamma) (hg1 : gamma ≤ 1)
    (he : 0 < epsilon) (he1 : epsilon < 1)
    (hscale : 4*(K:ℝ) ≤ alpha*gamma) (hnear : 4*(A.d:ℝ)*gamma*K ≤ epsilon/128)
    (hfar : (2:ℝ)^(-(3*K:ℕ):ℝ) ≤ epsilon/128)
    (hW : 20*A.d ≤ A.W) (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B)
    (hBK : 2*B ≤ K) (hK : 0 < K) :
    tableCount A ≤ CommonBasesFPRAS.slotTotal TwoLiftStates.pairs (f A alpha) ∅ ∧
      CommonBasesFPRAS.slotTotal TwoLiftStates.pairs (f A alpha) ∅ ≤ (1+epsilon/32)*tableCount A := by
…

Mentions: OAI.ContingencyTables.CompanionTerminalMass.Endpoints, OAI.ContingencyTables.CompanionTerminalMass.tableCount, OAI.CommonBasesFPRAS.slotTotal, OAI.ContingencyTables.TwoLiftStates.pairs