OAI/Analysis/FourierLLogL/Procedure/Score.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scoring surviving reference histories. We require evidence at successes only,

zeroing the score for regular successes without it.

  1. def OAI.FourierLLogL.Dyadic.Procedure.gate line 16
  2. def OAI.FourierLLogL.Dyadic.Procedure.sampleWinner line 20
  3. def OAI.FourierLLogL.Dyadic.Procedure.turnScore line 26
  4. def OAI.FourierLLogL.Dyadic.Procedure.Road.score line 37
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.score_nonneg line 43
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.total_gate line 61
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.stake_upper line 97