OAI/Probability/BinarySweep/Processes/IndependentHistory.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.independentHistory line 13
  2. lemma OAI.BinaryCoordinateSweeps.independentHistory_succ line 17
  3. lemma OAI.BinaryCoordinateSweeps.finiteLaw_independentHistory line 23
  4. def OAI.BinaryCoordinateSweeps.Assigns line 46
  5. lemma OAI.BinaryCoordinateSweeps.card_assignment_completions line 48
  6. lemma OAI.BinaryCoordinateSweeps.uniform_assignment_probability line 76
  7. lemma OAI.BinaryCoordinateSweeps.physicalLaw_eq_convolutionPower line 98
  8. def OAI.BinaryCoordinateSweeps.sweepHistory line 102
  9. lemma OAI.BinaryCoordinateSweeps.sweepLaw_eq_finiteLaw line 105
  10. def OAI.BinaryCoordinateSweeps.fromInitial line 108
  11. lemma OAI.BinaryCoordinateSweeps.totalVariation_fromInitial line 111
  12. theorem OAI.BinaryCoordinateSweeps.fixed_dimension_sweep_convergence_fromInitial line 119
  13. def OAI.BinaryCoordinateSweeps.ConstantSweepMixingTarget line 126
  14. def OAI.BinaryCoordinateSweeps.fallingCost line 132
  15. lemma OAI.BinaryCoordinateSweeps.fallingCost_sum line 134
  16. lemma OAI.BinaryCoordinateSweeps.fallingCost_nonneg line 149
  17. lemma OAI.BinaryCoordinateSweeps.prefix_sum_le_of_full_sum_le line 158
  18. lemma OAI.BinaryCoordinateSweeps.fallingCost_le line 179