OAI/Probability/Contingency/DenseWeightBounds.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Dense Weight Bounds.

  1. theorem OAI.Contingency.Dense.BinProblem.corner_penalty_bound line 17
  2. theorem OAI.Contingency.Dense.BinProblem.weight_upper line 58
  3. theorem OAI.Contingency.Dense.BinProblem.weight_lower line 64
  4. theorem OAI.Contingency.Dense.BinProblem.normalizer_upper line 73
  5. theorem OAI.Contingency.Dense.BinProblem.stationary_lower line 78
  6. def OAI.Contingency.Dense.BinProblem.inverseGap line 96
  7. theorem OAI.Contingency.Dense.BinProblem.inverseGap_eq line 98
  8. theorem OAI.Contingency.Dense.BinProblem.inverseGap_bounds line 105
  9. theorem OAI.Contingency.Dense.BinProblem.log_stationary_bound line 120
  10. theorem OAI.Contingency.Dense.BinProblem.prefactor_bound line 151
  11. theorem OAI.Contingency.Dense.BinProblem.scheduled_mixing line 164
  12. def OAI.Contingency.FiniteChain.Chain.invariant line 220
  13. def OAI.Contingency.FiniteChain.Chain.transition line 221
  14. def OAI.Contingency.FiniteChain.Chain.walk line 222
  15. theorem OAI.Contingency.FiniteChain.Chain.walk_mass line 226
  16. theorem OAI.Contingency.FiniteChain.Chain.walk_tv line 235
  17. def OAI.Contingency.Dense.BinProblem.idealSamples line 256
  18. def OAI.Contingency.Dense.BinProblem.decode line 258
  19. theorem OAI.Contingency.Dense.BinProblem.decode_eq_some line 262
  20. def OAI.Contingency.Dense.BinProblem.idealTrial line 281
  21. theorem OAI.Contingency.Dense.BinProblem.idealTrial_some line 283
  22. theorem OAI.Contingency.Dense.BinProblem.idealTrial_none line 289
  23. theorem OAI.Contingency.Dense.BinProblem.idealTrial_uniform line 299
  24. def OAI.Contingency.Dense.BinProblem.implementedOffsets line 309
  25. def OAI.Contingency.Dense.BinProblem.uniformOffsets line 312
  26. theorem OAI.Contingency.Dense.BinProblem.offset_tv line 315
  27. theorem OAI.Contingency.Dense.BinProblem.uniformOffsets_mass line 323
  28. theorem OAI.Contingency.Dense.BinProblem.idealSamples_prod line 331
  29. def OAI.Contingency.Dense.BinProblem.implementedTrial line 340
  30. theorem OAI.Contingency.Dense.BinProblem.implementedTrial_tv line 358
  31. theorem OAI.Contingency.square_le_two_pow line 396
  32. theorem OAI.Contingency.dense_schedule_offset line 408
  33. theorem OAI.Contingency.dense_schedule_failure line 436
  34. theorem OAI.Contingency.dense_schedule_total line 449
  35. def OAI.Contingency.Dense.BinProblem.draw line 476
  36. theorem OAI.Contingency.Dense.BinProblem.draw_tv line 481
  37. def OAI.Contingency.acceptCount line 509
  38. theorem OAI.Contingency.acceptCount_le line 511
  39. def OAI.Contingency.acceptCoin line 514
  40. theorem OAI.Contingency.acceptCoin_true line 522
  41. theorem OAI.Contingency.acceptCount_ratio line 526
  42. def OAI.Contingency.Law.accept line 548
  43. theorem OAI.Contingency.Law.accept_offdiag line 551
  44. theorem OAI.Contingency.Law.ext_offdiag line 556
  45. def OAI.Contingency.DyadicLaw.accept line 573
  46. theorem OAI.Contingency.DyadicLaw.toLaw_accept line 577
  47. def OAI.Contingency.DyadicLaw.neighborProposal line 597
  48. theorem OAI.Contingency.DyadicLaw.neighborProposal_offdiag line 610
  49. theorem OAI.Contingency.DyadicLaw.accepted_neighbor_kernel line 616
  50. def OAI.Contingency.proposalRate line 641
  51. theorem OAI.Contingency.proposalRate_bounds line 643
  52. theorem OAI.Contingency.binProposal_bounds line 665
  53. theorem OAI.Contingency.smallProposal_bounds line 671