OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseFinishSemantics.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionPhaseFinishProgram.data line 16
2. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.termInput_data line 20
3. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.term_value line 27
4. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.terms_data line 42
5. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.terms_den_pos line 54
6. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.ratio_data line 58
7. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.updated_entry line 73
8. def OAI.ContingencyTables.CompanionPhaseFinishProgram.view line 96

   Source documentation

   The relevant view of a physical stored value consists of its actual label-pair entries and its rational estimate.

   def view (z : Stored) : (Fin p→Fin p→ℚ)×ℚ :=
   …

   Mentions: OAI.ContingencyTables.CompanionPhaseFinishProgram.Stored

9. def OAI.ContingencyTables.CompanionPhaseFinishProgram.storedView line 99
10. def OAI.ContingencyTables.CompanionPhaseFinishProgram.rationalResult line 103

    Source documentation

    The phase result as a function of just the rational query values.

    def rationalResult (states : Fin N→Set (Labels A×Bool)) (old : CompanionPhaseWords.Stored A)
        (values : List (ℚ×ℚ)) : Option ((Fin p→Fin p→ℚ)×ℚ) :=
    …

    Mentions: OAI.ContingencyTables.CompanionPhaseWords.Stored

11. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.output_values line 112
12. theorem OAI.ContingencyTables.CompanionPhaseFinishProgram.output_update line 144

    Source documentation

    Applying the physical arithmetic and then reading its canonical entries is exactly the source update, including the abort outcome.

    theorem output_update (R : RootedCompletion.Selection A.T) (C K j : ℕ)
        (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ)
        (v : GridBoundary.Grid (I := Fin (CompanionOracleDensity.dimension A)) K)
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.CompanionOracleDensity.dimension

13. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.rationalResult_phase line 191