OAI/Combinatorics/ContingencyTables/Machines/CachedProfileDecision.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.ShortStep line 10
2. def OAI.ContingencyTables.ProfilePrograms.shortStepInput line 12
3. def OAI.ContingencyTables.ProfilePrograms.shortStepInputRealizer line 14
4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_shortStepInput line 17
5. def OAI.ContingencyTables.ProfilePrograms.cachedDecisionInput line 20
6. def OAI.ContingencyTables.ProfilePrograms.cachedDecisionInputRealizer line 23
7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_cachedDecisionInput line 30
8. def OAI.ContingencyTables.ProfilePrograms.cachedDecision line 38
9. def OAI.ContingencyTables.ProfilePrograms.cachedDecisionRealizer line 42
10. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_cachedDecision line 50
11. lemma OAI.ContingencyTables.ProfilePrograms.shortStep_candidate line 60

    Source documentation

    Changing only the completion bits cannot change the selected proposal.

    lemma shortStep_candidate (z : ProfileStepInput) :
        stepCandidateViews (shortStepInput (z.1,z.2.1))=stepCandidateViews z := rfl

    Mentions: OAI.ContingencyTables.ProfilePrograms.ProfileStepInput, OAI.ContingencyTables.ProfilePrograms.stepCandidateViews, OAI.ContingencyTables.ProfilePrograms.shortStepInput

12. lemma OAI.ContingencyTables.ProfilePrograms.cachedDecision_actual line 65

    Source documentation

    The exact test applied to a cached completion agrees with the implemented transition when that completion was actually drawn.

    lemma cachedDecision_actual (z : ProfileStepInput) :
        cachedDecision ((z.1,z.2.1),stepCompletion z)=profileStep z := rfl
    …

    Mentions: OAI.ContingencyTables.ProfilePrograms.ProfileStepInput, OAI.ContingencyTables.ProfilePrograms.cachedDecision, OAI.ContingencyTables.ProfilePrograms.stepCompletion, OAI.ContingencyTables.ProfilePrograms.profileStep