InitialMultiplierValues.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact source initial multipliers for actual labelled defects

lemma OAI.ContingencyTables.InitialMultiplierValues.bracket_hole_of_pos line 15
lemma OAI.ContingencyTables.InitialMultiplierValues.bracket_full_of_pos line 19
lemma OAI.ContingencyTables.InitialMultiplierValues.bracket_both_of_two line 26
lemma OAI.ContingencyTables.InitialMultiplierValues.same_cell_capacity line 35
def OAI.ContingencyTables.InitialMultiplierValues.value line 47
lemma OAI.ContingencyTables.InitialMultiplierValues.value_positive line 51
lemma OAI.ContingencyTables.InitialMultiplierValues.bracket_product_same line 55
lemma OAI.ContingencyTables.InitialMultiplierValues.bracket_product_different line 73

theorem OAI.ContingencyTables.InitialMultiplierValues.ideal_constant line 100

Source documentation

The exact finite transversal/defect ratio is six in a shared cell, and otherwise six times (b_hole+1)/(b_full+2).

theorem ideal_constant [DecidableEq C] (p q : Copy b) (hpq : p≠q) (M : ℝ) (hM : 0< M) :
    slotTotal pairs (LabelledFactorial.firstLift (group (cell b)) (fun _ => M)
      (InitialTransversals.denominator b)) ∅/
      slotDefect pairs (LabelledFactorial.firstLift (group (cell b)) (fun _ => M)
        (InitialTransversals.denominator b)) ∅ (TwoLiftStates.pair p) (TwoLiftStates.pair q)=value b p q := by
…

Mentions: OAI.ContingencyTables.LabelledFactorial.firstLift, OAI.ContingencyTables.InitialTransversals.denominator, OAI.ContingencyTables.TwoLiftStates.pair, OAI.ContingencyTables.InitialMultiplierValues.value

def OAI.ContingencyTables.CompanionInitialMultipliers.multiplier line 125
lemma OAI.ContingencyTables.CompanionInitialMultipliers.multiplier_positive line 129
lemma OAI.ContingencyTables.CompanionInitialMultipliers.freeTotal_positive line 132
theorem OAI.ContingencyTables.CompanionInitialMultipliers.ideal_at_zero line 139
Source documentation
The explicit rational initial multiplier equals the ideal for the literal source count, not just for an abstract constant lift.
```
theorem ideal_at_zero (A : Instance I J) (p q : Labels A) (hpq : p≠q) :
    slotTotal pairs (f A 0) ∅/slotDefect pairs (f A 0) ∅ (TwoLiftStates.pair p) (TwoLiftStates.pair q)=
      multiplier A (TwoLiftStates.pair p) (TwoLiftStates.pair q) := by
…
```
Mentions: OAI.ContingencyTables.TwoLiftStates.pair, OAI.ContingencyTables.CompanionInitialMultipliers.multiplier
theorem OAI.ContingencyTables.CompanionInitialMultipliers.initial_good line 154
Source documentation
Initialization has exact ideals, hence satisfies every good- multiplier inequality for the actual chain without a sampling event.
```
theorem initial_good (A : Instance I J) : GoodMultipliers pairs (f A 0) (multiplier A) := by
…
```
Mentions: OAI.ContingencyTables.CompanionInitialMultipliers.multiplier