OAI/Combinatorics/ContingencyTables/Rooted/RootedZeroLabels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Counting when the retained small cells have no positive capacities

The paired transversal space then has one state. The terminal total is one actual free-assignment weight, so the bounded-word weight estimator applies directly; no Markov restart is needed.

  1. lemma OAI.ContingencyTables.RootedZeroLabels.small_capacity_zero line 23
  2. lemma OAI.ContingencyTables.RootedZeroLabels.profile_zero line 29
  3. lemma OAI.ContingencyTables.RootedZeroLabels.factorialRatio_one line 36
  4. lemma OAI.ContingencyTables.RootedZeroLabels.total_eq_h line 42
  5. theorem OAI.ContingencyTables.RootedZeroLabels.success line 55

    Source documentation

    The direct all-large branch has arbitrary confidence using the same actual finite-word evaluator, with no positive-label premise.

    theorem success (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (hzero : Fintype.card (Labels A)=0) (E : Endpoints A)
    (C K L : ℕ) (hC : 0 < C) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (hB : (K:ℝ)=binWidth A C) (hW' : 20*A.d ≤ A.W)
    (epsilon delta : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1) (hd : 0 < delta)
    (hL : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^L)
    (hH : finalPhase A L (epsilon:ℝ) ≤ rationalHeight A C)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger