OAI/Computability/DirectedFeedback/Games/Harmonic.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Gadget.Harmonic.harmonic line 12
  2. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_zero line 16
  3. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_succ line 18
  4. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_eq_sum line 21
  5. def OAI.DFVSGames.Gadget.Harmonic.average line 27
  6. def OAI.DFVSGames.Gadget.Harmonic.probability line 29
  7. theorem OAI.DFVSGames.Gadget.Harmonic.average_mono line 32
  8. theorem OAI.DFVSGames.Gadget.Harmonic.average_nonneg line 36
  9. theorem OAI.DFVSGames.Gadget.Harmonic.average_const line 40
  10. theorem OAI.DFVSGames.Gadget.Harmonic.average_add line 44
  11. theorem OAI.DFVSGames.Gadget.Harmonic.average_sub line 48
  12. theorem OAI.DFVSGames.Gadget.Harmonic.average_mul_left line 52
  13. theorem OAI.DFVSGames.Gadget.Harmonic.probability_nonneg line 56
  14. theorem OAI.DFVSGames.Gadget.Harmonic.probability_le_one line 62
  15. theorem OAI.DFVSGames.Gadget.Harmonic.probability_mono line 71
  16. theorem OAI.DFVSGames.Gadget.Harmonic.probability_not line 80
  17. theorem OAI.DFVSGames.Gadget.Harmonic.probability_eq_half_of_swap line 89
  18. theorem OAI.DFVSGames.Gadget.Harmonic.binary_character_detection_probability line 99
  19. theorem OAI.DFVSGames.Gadget.Harmonic.binary_family_detection_ge_half line 116
  20. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_nonneg line 124
  21. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_mono line 129
  22. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_pos line 137
  23. theorem OAI.DFVSGames.Gadget.Harmonic.harmonic_sub_predecessor line 142
  24. theorem OAI.DFVSGames.Gadget.Harmonic.generic_drop_identity line 147
  25. theorem OAI.DFVSGames.Gadget.Harmonic.generic_expected_drop_le line 161
  26. theorem OAI.DFVSGames.Gadget.Harmonic.arbitrary_expected_drop_le line 173
  27. theorem OAI.DFVSGames.Gadget.Harmonic.expected_drop_le_four_theta line 192
  28. def OAI.DFVSGames.Gadget.Harmonic.badRankCoefficient line 209
  29. theorem OAI.DFVSGames.Gadget.Harmonic.badRankCoefficient_nonneg line 211
  30. def OAI.DFVSGames.Gadget.Harmonic.depth line 214
  31. theorem OAI.DFVSGames.Gadget.Harmonic.depth_budget line 216
  32. theorem OAI.DFVSGames.Gadget.Harmonic.expected_total_drop_le line 224
  33. theorem OAI.DFVSGames.Gadget.Harmonic.survival_probability_ge_half_of_potential line 245
  34. theorem OAI.DFVSGames.Gadget.Harmonic.survival_probability_ge_half line 266
  35. theorem OAI.DFVSGames.Gadget.Harmonic.survival_of_adaptive_step_law line 278
  36. theorem OAI.DFVSGames.Gadget.Harmonic.detection_probability_ge_quarter line 301
  37. theorem OAI.DFVSGames.Gadget.Harmonic.probability_product line 320
  38. theorem OAI.DFVSGames.Gadget.Harmonic.product_detection_probability_ge_quarter line 328
  39. theorem OAI.DFVSGames.Gadget.Harmonic.binary_product_detection_probability_ge_quarter line 340
  40. theorem OAI.DFVSGames.Quadratic.exists_nonzero_kernel_of_range_rank_lt_inline_HarmonicLoss line 362
  41. theorem OAI.DFVSGames.Quadratic.probability_rank_drop_le_loss_count_inline_HarmonicLoss line 379
  42. def OAI.DFVSGames.Quadratic.fieldLineTheta line 406
  43. theorem OAI.DFVSGames.Quadratic.fieldLineTheta_eq line 410
  44. def OAI.DFVSGames.Quadratic.nextBlockRank line 414
  45. theorem OAI.DFVSGames.Quadratic.nextBlockRank_le line 419
  46. theorem OAI.DFVSGames.Quadratic.nextBlockRank_independent line 424
  47. theorem OAI.DFVSGames.Quadratic.generic_nextBlockRank_dichotomy line 436
  48. theorem OAI.DFVSGames.Quadratic.generic_block_loss_probability_le line 448
  49. theorem OAI.DFVSGames.Quadratic.generic_block_harmonic_loss_le line 463
  50. theorem OAI.DFVSGames.Quadratic.card_loss_fieldLineRestrictions_le_nonzero line 485
  51. theorem OAI.DFVSGames.Quadratic.arbitrary_block_loss_probability_le line 500
  52. theorem OAI.DFVSGames.Quadratic.arbitrary_block_harmonic_loss_le line 520
  53. def OAI.DFVSGames.Gadget.OutgoingHarmonic.outgoingLoss line 546
  54. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.outgoingLoss_eq_line_average line 551
  55. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.generic_outgoing_loss_le line 571
  56. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.arbitrary_outgoing_loss_le line 579
  57. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.badRankCoefficient_mono line 587
  58. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.outgoing_harmonic_loss_le line 594
  59. theorem OAI.DFVSGames.Gadget.OutgoingHarmonic.descendant_harmonic_loss_le line 613
  60. def OAI.DFVSGames.Quadratic.nongenericFraction line 640
  61. def OAI.DFVSGames.Gadget.FreshGenericity.rankSpaceEquiv line 662
  62. theorem OAI.DFVSGames.Gadget.FreshGenericity.rankSpaceEquiv_apply line 667
  63. def OAI.DFVSGames.Gadget.FreshGenericity.bad line 689
  64. theorem OAI.DFVSGames.Gadget.FreshGenericity.mean_bad_rankSpace line 692
  65. theorem OAI.DFVSGames.Gadget.FreshGenericity.mean_fresh_bad_at_line line 711
  66. theorem OAI.DFVSGames.Gadget.FreshGenericity.unoriented_rank_le line 735
  67. theorem OAI.DFVSGames.Gadget.FreshGenericity.fresh_bad_at_line_le line 744
  68. theorem OAI.DFVSGames.Gadget.FreshGenericity.fresh_bad_le line 756
  69. theorem OAI.DFVSGames.Gadget.FreshGenericity.descendant_bad_le line 771