OAI/Combinatorics/ContingencyTables/Counting/CompanionTraceWords.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Capped trace returns from the actual companion Boolean walk

The return search scans the recorded path after its initial state. Its reference expectation is the finite Green sum defining the capped trace; the Boolean walk contributes its path error.

  1. def OAI.ContingencyTables.CompanionTraceWords.eventIndicator line 26

    Source documentation

    A fixed indicator convention keeps equivalent event descriptions independent of the decision procedures inferred for their propositions.

    def eventIndicator (P : Prop) : ℝ := @ite ℝ P (Classical.propDecidable P) 1 0
  2. lemma OAI.ContingencyTables.CompanionTraceWords.eventIndicator_eq line 28
  3. def OAI.ContingencyTables.CompanionTraceWords.firstHit line 32
  4. def OAI.ContingencyTables.CompanionTraceWords.returnValue line 36
  5. lemma OAI.ContingencyTables.CompanionTraceWords.expectation_congr_start line 41
  6. lemma OAI.ContingencyTables.CompanionTraceWords.firstHit_expectation line 52
  7. lemma OAI.ContingencyTables.CompanionTraceWords.returnValue_succ line 69
  8. lemma OAI.ContingencyTables.CompanionTraceWords.returnValue_split line 79
  9. lemma OAI.ContingencyTables.CompanionTraceWords.partialGreen_succ line 93
  10. theorem OAI.ContingencyTables.CompanionTraceWords.outside_return_expectation line 102

    Source documentation

    An outside starting state has exactly the truncated Green expectation.

    theorem outside_return_expectation (C : FiniteChain X) (B : X → Prop)
    (Q : KilledKernel (FiniteChain.Outside B))
    (hQ : ∀ x y,Q.Q x y=C.P x.val y.val)
    (phi : FiniteChain.Inside B → ℝ) (n : ℕ) (x : FiniteChain.Outside B) :
    C.pathExpectation n x.val (returnValue B phi)=
      Q.partialGreen n (fun z => ∑ y : FiniteChain.Inside B,C.P z.val y.val*phi y) x := by
…

    Mentions: OAI.ContingencyTables.CompanionTraceWords.returnValue

  11. theorem OAI.ContingencyTables.CompanionTraceWords.inside_return_expectation line 121

    Source documentation

    Starting inside and allowing n+1 transitions gives the manuscript's capped trace, with n possible further outside transitions.

    theorem inside_return_expectation (C : FiniteChain X) (B : X → Prop)
    (Q : KilledKernel (FiniteChain.Outside B))
    (hQ : ∀ x y,Q.Q x y=C.P x.val y.val)
    (phi : FiniteChain.Inside B → ℝ) (n : ℕ) (x : FiniteChain.Inside B) :
    C.pathExpectation (n+1) x.val (returnValue B phi)=
      ∑ y : FiniteChain.Inside B,C.cappedTrace B Q n x y*phi y := by
…

    Mentions: OAI.ContingencyTables.CompanionTraceWords.returnValue

  12. lemma OAI.ContingencyTables.CompanionTraceWords.option_event line 147
  13. theorem OAI.ContingencyTables.CompanionTraceWords.return_event_expectation line 153
  14. theorem OAI.ContingencyTables.CompanionTraceWords.return_failure_expectation line 167
  15. def OAI.ContingencyTables.CompanionTraceWords.sourceKilled line 188
  16. def OAI.ContingencyTables.CompanionTraceWords.targetKilled line 195
  17. lemma OAI.ContingencyTables.CompanionTraceWords.targetKilled_matches line 201
  18. def OAI.ContingencyTables.CompanionTraceWords.returnWord line 210

    Source documentation

    The search consumes a fixed cap worth of disjoint words even when the first return occurs before the last word.

    def returnWord (A : Instance I J) (C K j k N : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ) (S : State A)
…
  19. lemma OAI.ContingencyTables.CompanionTraceWords.arithmetic_event_eq line 218
  20. theorem OAI.ContingencyTables.CompanionTraceWords.arithmetic_recorded_event_bound line 238
  21. theorem OAI.ContingencyTables.CompanionTraceWords.returnWord_event line 256

    Source documentation

    The concrete bounded return experiment has the capped trace event bound plus one implementation error per used step.

    theorem returnWord_event (A : Instance I J) (C : ℕ) (hC : 0<C) (K j k n : ℕ)
    (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

  22. theorem OAI.ContingencyTables.CompanionTraceWords.returnWord_failure line 280

    Source documentation

    Capping the concrete word experiment adds the exact reference nonreturn probability and the accumulated step-implementation error.

    theorem returnWord_failure (A : Instance I J) (C : ℕ) (hC : 0<C) (K j k n : ℕ)
    (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