OAI/Computability/DirectedFeedback/Games/A5ForwardIndex.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.quotient_relativeFrequency_apply line 16
  2. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.quotient_compress_apply line 28
  3. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_of_pointwise line 35
  4. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.quotientFactor_mapQ line 52
  5. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.dualFactor_quotient line 62
  6. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.outputFactor_symm_as_inclusion line 73
  7. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_dualFactor line 83
  8. theorem OAI.DFVSGames.Appendix.A5FrequencyTransport.isAntecedent_relativeFrequency_dualFactor line 100
  9. abbrev OAI.DFVSGames.Appendix.A5ForwardIndex.Index line 133
  10. def OAI.DFVSGames.Appendix.A5ForwardIndex.descendant line 137
  11. def OAI.DFVSGames.Appendix.A5ForwardIndex.sourceI line 143
  12. def OAI.DFVSGames.Appendix.A5ForwardIndex.sourceJ line 146
  13. def OAI.DFVSGames.Appendix.A5ForwardIndex.targetRank line 149
  14. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.descendant_rank line 153
  15. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.original_size line 158
  16. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.original_order_bounds line 164
  17. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.descendant_size_le line 171
  18. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.earlierA_le line 177
  19. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.earlierB_le line 185
  20. abbrev OAI.DFVSGames.Appendix.A5ForwardIndex.Fiber line 190
  21. def OAI.DFVSGames.Appendix.A5ForwardIndex.encode line 194
  22. def OAI.DFVSGames.Appendix.A5ForwardIndex.earlierTriple line 205
  23. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.earlierTriple_encode line 212
  24. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.encode_injective line 221
  25. theorem OAI.DFVSGames.Appendix.A5ForwardIndex.card_fiber_le line 250
  26. theorem OAI.DFVSGames.Appendix.A5WeightedReindex.exponent_weight_le line 283
  27. theorem OAI.DFVSGames.Appendix.A5WeightedReindex.counted_weight_le line 298
  28. def OAI.DFVSGames.Appendix.A5WeightedReindex.fiber line 315
  29. theorem OAI.DFVSGames.Appendix.A5WeightedReindex.sum_grouped line 318
  30. theorem OAI.DFVSGames.Appendix.A5WeightedReindex.weighted_reindex line 338
  31. def OAI.DFVSGames.Appendix.A5ReverseSum.actualMoment line 444
  32. def OAI.DFVSGames.Appendix.A5ReverseSum.targetWeight line 448
  33. theorem OAI.DFVSGames.Appendix.A5ReverseSum.targetWeight_nonneg line 453
  34. theorem OAI.DFVSGames.Appendix.A5ReverseSum.targetWeight_descendant line 460
  35. theorem OAI.DFVSGames.Appendix.A5ReverseSum.sum_triples_cutoff line 471
  36. theorem OAI.DFVSGames.Appendix.A5ReverseSum.target_sum_eq line 502
  37. theorem OAI.DFVSGames.Appendix.A5ReverseSum.source_summand_eq line 533
  38. theorem OAI.DFVSGames.Appendix.A5ReverseSum.source_sum_eq line 543
  39. theorem OAI.DFVSGames.Appendix.A5ReverseSum.weighted_descendantSum_le line 562
  40. def OAI.DFVSGames.Appendix.A5Induction.BoundAtDegree line 598
  41. theorem OAI.DFVSGames.Appendix.A5Induction.damping_le line 608
  42. theorem OAI.DFVSGames.Appendix.A5Induction.coefficient_absorption line 626
  43. def OAI.DFVSGames.Appendix.A5Induction.dampedMapMoment line 663
  44. theorem OAI.DFVSGames.Appendix.A5Induction.dampedMapMoment_le line 668
  45. def OAI.DFVSGames.Appendix.A5Induction.dampedHybridMoment line 694
  46. theorem OAI.DFVSGames.Appendix.A5Induction.dampedHybridMoment_le line 698
  47. theorem OAI.DFVSGames.Appendix.A5Induction.hybridProjector_zero_pair line 717
  48. theorem OAI.DFVSGames.Appendix.A5Induction.energy_sq_le_hybridMomentSum line 723
  49. theorem OAI.DFVSGames.Appendix.A5Induction.degree_zero_bound line 758
  50. theorem OAI.DFVSGames.Appendix.A5Induction.recurrence_closure line 763
  51. theorem OAI.DFVSGames.Appendix.A5Induction.lifted_outer_dimensions line 798
  52. theorem OAI.DFVSGames.Appendix.A5Induction.a5_energySquare_le_power line 812
  53. def OAI.DFVSGames.Appendix.A5Induction.postA5Sum line 877
  54. theorem OAI.DFVSGames.Appendix.A5Induction.mapDerivative_hybridMomentSum_le line 882
  55. theorem OAI.DFVSGames.Appendix.A5Induction.postA5Sum_hybrid_average line 907
  56. theorem OAI.DFVSGames.Appendix.A5Induction.a15_of_strong_induction line 924
  57. theorem OAI.DFVSGames.Appendix.A5Induction.boundedTripleSum_le_descendants line 960
  58. theorem OAI.DFVSGames.Appendix.A5Induction.boundAtDegree line 995
  59. theorem OAI.DFVSGames.Appendix.A5Induction.derivative_inequality line 1019