OAI/Computability/BinPacking/PCP/PoweringMomentBound.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.PoweringMoment.bit line 18
  2. def OAI.BinPackingGames.Foundations.PCP.PoweringMoment.hits line 22
  3. def OAI.BinPackingGames.Foundations.PCP.PoweringMoment.mean line 25
  4. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.bit_nonneg line 27
  5. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.bit_sq line 31
  6. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.bit_mul line 35
  7. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.bit_mono line 39
  8. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.hits_nonneg line 47
  9. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.mean_nonneg line 50
  10. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.mean_hits line 53
  11. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.second_moment_eq line 57
  12. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 65
  13. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMoment.rejection_lower_bound line 97
  14. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.lazyRotate line 124
  15. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 128
  16. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.lazyGraph line 136
  17. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 144
  18. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 147
  19. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 158
  20. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 166
  21. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 178
  22. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 192
  23. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 207
  24. def OAI.BinPackingGames.Foundations.PCP.PoweringReturn.portConsEquiv line 228
  25. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 241
  26. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 249
  27. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 257
  28. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 264
  29. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 285
  30. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 327
  31. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.bit_bool line 351
  32. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 354
  33. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 358
  34. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 368
  35. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 372
  36. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.word_hit_mean line 383
  37. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 410
  38. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.hit_mean line 468
  39. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 484
  40. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReturn.pair_event_mean line 505
  41. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWitness.iterate_mul_const line 522
  42. def OAI.BinPackingGames.Foundations.PCP.PoweringWitness.endpointWitness line 535
  43. def OAI.BinPackingGames.Foundations.PCP.PoweringWitness.vertexWitness line 541
  44. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 546
  45. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 581
  46. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 621
  47. def OAI.BinPackingGames.Foundations.PCP.PoweringMomentBound.windowIndex line 676
  48. def OAI.BinPackingGames.Foundations.PCP.PoweringMomentBound.windowEvent line 681
  49. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 685
  50. theorem OAI.BinPackingGames.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 709