OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseTrajectory.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The observed Boolean trajectory has the source path law

The finite history stores the visited prefix. Its exact real reference expectation is the manuscript's list-path expectation, so the row error controls events involving all empirical observations simultaneously.

  1. def OAI.ContingencyTables.CompanionPhaseTrajectory.historyPrefix line 25
  2. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_nonempty line 29
  3. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_last line 32
  4. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_end line 40
  5. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.read_put line 45
  6. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.position_put line 48
  7. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_put line 52
  8. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_initial line 71
  9. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.power_succ_left line 76
  10. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.power_expectation_succ line 86
  11. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.lift_expectation line 93
  12. theorem OAI.ContingencyTables.CompanionPhaseTrajectory.prefix_expectation line 105

    Source documentation

    Before saturation, the finite lifted chain has exactly the usual list-path expectation, with the observed prefix retained.

    theorem prefix_expectation (C : FiniteChain X) (N n : ℕ)
    (a : PathState X N) (hn : a.1.val+n≤N) (F : List X → ℝ) :
    (∑ b,((liftKernel C.kernel pathRead pathPut).power n).P a b*F (historyPrefix b))=
      C.pathExpectation n (pathRead a) (fun l => F ((historyPrefix a).dropLast++l)) := by
…

    Mentions: OAI.ContingencyTables.CompanionPhaseTrajectory.historyPrefix

  13. theorem OAI.ContingencyTables.CompanionPhaseTrajectory.initial_prefix_expectation line 139
  14. lemma OAI.ContingencyTables.CompanionPhaseTrajectory.event_le_distance line 146
  15. theorem OAI.ContingencyTables.CompanionPhaseTrajectory.recorded_event_bound line 159

    Source documentation

    Every event of the actual observed Boolean trajectory is bounded by the source list-path event plus one proved row error per transition.

    theorem recorded_event_bound (A : Instance I J) (C : ℕ) (hC : 0<C) (K j k : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

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