OAI/Computability/DirectedFeedback/Probability/A13Reduction.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Appendix.A13Reduction.exponent_le line 18
  2. theorem OAI.DFVSGames.Appendix.A13Reduction.weighted_moment_le line 28
  3. def OAI.DFVSGames.Appendix.A13Reduction.tripleMoment line 49
  4. theorem OAI.DFVSGames.Appendix.A13Reduction.tripleMoment_nonneg line 54
  5. theorem OAI.DFVSGames.Appendix.A13Reduction.weak_fourth_le_counted line 62
  6. theorem OAI.DFVSGames.Appendix.A13Reduction.weighted_weak_fourth_le_counted line 80
  7. theorem OAI.DFVSGames.Appendix.A13Reduction.tripleMoment_eq_zero_of_lt_size line 95
  8. def OAI.DFVSGames.Appendix.A13Reduction.tripleTerm line 102
  9. theorem OAI.DFVSGames.Appendix.A13Reduction.tripleTerm_nonneg line 107
  10. theorem OAI.DFVSGames.Appendix.A13Reduction.tripleTerm_eq_zero_of_lt_size line 111
  11. theorem OAI.DFVSGames.Appendix.A13Reduction.weighted_geometric_moment_le line 118
  12. def OAI.DFVSGames.Appendix.A13Reduction.positiveTripleSum line 138
  13. def OAI.DFVSGames.Appendix.A13Reduction.boundedPositiveTripleSum line 141
  14. theorem OAI.DFVSGames.Appendix.A13Reduction.weakFourthSum_le_positiveTripleSum line 144
  15. theorem OAI.DFVSGames.Appendix.A13Reduction.positiveTripleSum_eq_bounded line 176
  16. theorem OAI.DFVSGames.Appendix.A13Reduction.degree_reduction line 197
  17. theorem OAI.DFVSGames.Appendix.A13Reduction.degree_reduction_truncated line 204
  18. def OAI.DFVSGames.Appendix.DerivativeInduction.IsAntecedent line 222
  19. abbrev OAI.DFVSGames.Appendix.DerivativeInduction.Antecedent line 227
  20. theorem OAI.DFVSGames.Appendix.DerivativeInduction.antecedent_image_from_left line 230
  21. theorem OAI.DFVSGames.Appendix.DerivativeInduction.antecedent_bottom_mem_range line 243
  22. theorem OAI.DFVSGames.Appendix.DerivativeInduction.antecedent_vertical_zero line 249
  23. theorem OAI.DFVSGames.Appendix.DerivativeInduction.antecedent_kernel_le_inline_DerivativeInduction line 255
  24. def OAI.DFVSGames.Appendix.DerivativeInduction.graphParameter line 263
  25. theorem OAI.DFVSGames.Appendix.DerivativeInduction.graphParameter_apply line 269
  26. def OAI.DFVSGames.Appendix.DerivativeInduction.complementParameter line 275
  27. theorem OAI.DFVSGames.Appendix.DerivativeInduction.complementParameter_val line 280
  28. def OAI.DFVSGames.Appendix.DerivativeInduction.lift line 284
  29. theorem OAI.DFVSGames.Appendix.DerivativeInduction.lift_apply line 289
  30. theorem OAI.DFVSGames.Appendix.DerivativeInduction.lift_isAntecedent line 294
  31. def OAI.DFVSGames.Appendix.DerivativeInduction.intoAntecedent line 319
  32. theorem OAI.DFVSGames.Appendix.DerivativeInduction.graphParameter_lift line 324
  33. theorem OAI.DFVSGames.Appendix.DerivativeInduction.complementParameter_lift line 332
  34. theorem OAI.DFVSGames.Appendix.DerivativeInduction.lift_parameters line 338
  35. def OAI.DFVSGames.Appendix.DerivativeInduction.antecedentEquiv line 357
  36. def OAI.DFVSGames.Appendix.DerivativeInduction.graphEmbedding line 366
  37. theorem OAI.DFVSGames.Appendix.DerivativeInduction.graphEmbedding_injective line 369
  38. theorem OAI.DFVSGames.Appendix.DerivativeInduction.range_lift line 374
  39. theorem OAI.DFVSGames.Appendix.DerivativeInduction.finrank_range_lift line 386
  40. theorem OAI.DFVSGames.Appendix.DerivativeInduction.finrank_range_antecedent line 392
  41. theorem OAI.DFVSGames.Appendix.DerivativeInduction.card_antecedent line 398
  42. theorem OAI.DFVSGames.Appendix.DerivativeInduction.isAntecedent_iff_pointwise line 408
  43. theorem OAI.DFVSGames.Appendix.DerivativeInduction.disjoint_range_iff_zero line 432
  44. theorem OAI.DFVSGames.Appendix.DerivativeInduction.sup_kernel_iff_image line 442
  45. def OAI.DFVSGames.Appendix.DerivativeInduction.IsSubspaceAntecedent line 462
  46. abbrev OAI.DFVSGames.Appendix.DerivativeInduction.SubspaceAntecedent line 467
  47. def OAI.DFVSGames.Appendix.DerivativeInduction.coordinateEquiv line 471
  48. theorem OAI.DFVSGames.Appendix.DerivativeInduction.coordinateEquiv_apply line 477
  49. theorem OAI.DFVSGames.Appendix.DerivativeInduction.coordinate_antecedent_iff line 483
  50. def OAI.DFVSGames.Appendix.DerivativeInduction.subspaceAntecedentEquiv line 529
  51. theorem OAI.DFVSGames.Appendix.DerivativeInduction.card_subspaceAntecedent line 538
  52. def OAI.DFVSGames.Appendix.AntecedentCount.IsAntecedent line 564
  53. abbrev OAI.DFVSGames.Appendix.AntecedentCount.Antecedent line 568
  54. abbrev OAI.DFVSGames.Appendix.AntecedentCount.Admissible line 572
  55. def OAI.DFVSGames.Appendix.AntecedentCount.compressionEquiv line 575
  56. theorem OAI.DFVSGames.Appendix.AntecedentCount.isAntecedent_iff_subspace line 585
  57. def OAI.DFVSGames.Appendix.AntecedentCount.subspaceEquiv line 603
  58. theorem OAI.DFVSGames.Appendix.AntecedentCount.rank_eq line 615
  59. theorem OAI.DFVSGames.Appendix.AntecedentCount.card_antecedent line 622
  60. theorem OAI.DFVSGames.Appendix.AntecedentCount.card_antecedent_le line 634
  61. theorem OAI.DFVSGames.Appendix.AntecedentCount.sum_compression line 648
  62. abbrev OAI.DFVSGames.Appendix.A5ReverseIndex.EarlierA line 684
  63. abbrev OAI.DFVSGames.Appendix.A5ReverseIndex.EarlierB line 687
  64. def OAI.DFVSGames.Appendix.A5ReverseIndex.frequencyEquiv line 690
  65. def OAI.DFVSGames.Appendix.A5ReverseIndex.relativeFrequency line 698
  66. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.relativeFrequency_rank line 702
  67. abbrev OAI.DFVSGames.Appendix.A5ReverseIndex.Ancestor line 711
  68. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.relative_codomain_dimension line 719
  69. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.relative_domain_codimension_le line 728
  70. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.card_local_antecedent_le line 738
  71. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.card_sigma_le_inline_A5ReverseIndex line 762
  72. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.card_ancestor_le line 774
  73. theorem OAI.DFVSGames.Appendix.A5ReverseIndex.card_ancestor_le_source line 803