OAI/Computability/DirectedFeedback/Games/A5Scalar.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Appendix.Induction.outer_order_cutoff line 8
2. theorem OAI.DFVSGames.Appendix.Induction.complement_dimension_bounds line 14
3. theorem OAI.DFVSGames.Appendix.Induction.recombined_order_cutoff line 19
4. theorem OAI.DFVSGames.Appendix.Induction.square_remainder_budget line 24
5. theorem OAI.DFVSGames.Appendix.Induction.induction_exponent_budget line 33
6. theorem OAI.DFVSGames.Appendix.Induction.antecedent_exponent_budget line 40
7. theorem OAI.DFVSGames.Appendix.Induction.first_triangle_exponent_budget line 49
8. theorem OAI.DFVSGames.Appendix.Induction.initial_order_bound line 55
9. theorem OAI.DFVSGames.Appendix.Induction.positive_rank_geometric_slack line 59
10. theorem OAI.DFVSGames.Appendix.Induction.corrected_weight_exponent line 65
11. theorem OAI.DFVSGames.Appendix.Induction.extension_unique line 71
12. theorem OAI.DFVSGames.Appendix.A5Scalar.absorption line 92
13. theorem OAI.DFVSGames.Appendix.A5Scalar.geometric_sum_le line 116
14. def OAI.DFVSGames.Appendix.A5Scalar.positiveSum line 125
15. theorem OAI.DFVSGames.Appendix.A5Scalar.pair_sum_factor line 129
16. theorem OAI.DFVSGames.Appendix.A5Scalar.positiveSum_zero_eq line 136
17. theorem OAI.DFVSGames.Appendix.A5Scalar.positiveSum_zero_le line 161
18. theorem OAI.DFVSGames.Appendix.A5Scalar.positiveSum_pos_le line 174
19. theorem OAI.DFVSGames.Appendix.A5Scalar.a16_finite_geometric line 191
20. theorem OAI.DFVSGames.Appendix.A5Scalar.a16_original_range line 230
21. abbrev OAI.DFVSGames.Appendix.A5Passage.OuterIndex line 252
22. def OAI.DFVSGames.Appendix.A5Passage.LiftedA line 255
23. def OAI.DFVSGames.Appendix.A5Passage.LiftedB line 258
24. abbrev OAI.DFVSGames.Appendix.A5Passage.Pair line 261
25. abbrev OAI.DFVSGames.Appendix.A5Passage.Passage line 264
26. theorem OAI.DFVSGames.Appendix.A5Passage.comap_mkQ_injective line 267
27. theorem OAI.DFVSGames.Appendix.A5Passage.map_subtype_injective line 276
28. theorem OAI.DFVSGames.Appendix.A5Passage.outer_eq_of_lifted line 297
29. theorem OAI.DFVSGames.Appendix.A5Passage.recover_liftedA line 302
30. theorem OAI.DFVSGames.Appendix.A5Passage.recover_liftedB line 305
31. def OAI.DFVSGames.Appendix.A5Passage.forget line 308
32. theorem OAI.DFVSGames.Appendix.A5Passage.forget_injective line 311
33. theorem OAI.DFVSGames.Appendix.A5Passage.forget_val line 331
34. instance OAI.DFVSGames.Appendix.A5Passage.pairFintype line 336
35. theorem OAI.DFVSGames.Appendix.A5Passage.dim_pairA line 348
36. theorem OAI.DFVSGames.Appendix.A5Passage.codim_pairB line 358
37. theorem OAI.DFVSGames.Appendix.A5Passage.pair_order line 372
38. theorem OAI.DFVSGames.Appendix.A5Passage.pair_order_le line 379
39. theorem OAI.DFVSGames.Appendix.A5Passage.pair_rank line 386
40. theorem OAI.DFVSGames.Appendix.A5Passage.descendant_rank line 394
41. theorem OAI.DFVSGames.Appendix.A5Passage.effective_order_rank line 403
42. theorem OAI.DFVSGames.Appendix.A5Passage.effective_order_rank_le line 416
43. theorem OAI.DFVSGames.Appendix.A5Passage.effective_order_rank_pos line 432
44. def OAI.DFVSGames.Appendix.A5Passage.descendantSum line 443
45. theorem OAI.DFVSGames.Appendix.A5Passage.descendantSum_nonneg line 452
46. theorem OAI.DFVSGames.Appendix.F1Gram.gram_energy_le line 463
47. theorem OAI.DFVSGames.Appendix.F1Gram.sum_subtype_eq line 478
48. theorem OAI.DFVSGames.Appendix.F1Gram.sum_comp_le line 495
49. def OAI.DFVSGames.Appendix.SubspaceExtensions.horizontal line 513
50. def OAI.DFVSGames.Appendix.SubspaceExtensions.hKernel line 514
51. def OAI.DFVSGames.Appendix.SubspaceExtensions.scalarMap line 516
52. def OAI.DFVSGames.Appendix.SubspaceExtensions.extension line 521
53. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.extension_mem line 525
54. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mkQ_eq_smul_iff line 530
55. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.hKernel_horizontal line 537
56. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.hKernel_extension line 542
57. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.exists_one_extension line 549
58. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.eq_extension_of_one_mem line 553
59. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.eq_horizontal_of_no_one line 567
60. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.horizontal_ne_extension line 586
61. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.extension_injective line 593
62. def OAI.DFVSGames.Appendix.SubspaceExtensions.encode line 601
63. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.encode_injective line 605
64. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.encode_surjective line 629
65. def OAI.DFVSGames.Appendix.SubspaceExtensions.splitEquiv line 636
66. def OAI.DFVSGames.Appendix.SubspaceExtensions.horizontalEquiv line 639
67. def OAI.DFVSGames.Appendix.SubspaceExtensions.extensionEquiv line 652
68. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.finrank_horizontal line 692
69. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.finrank_extension line 695
70. def OAI.DFVSGames.Appendix.SubspaceExtensions.weightedTotal line 709
71. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.card_eq_pow_finrank line 711
72. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.quotient_card_mul_pow line 719
73. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.weightedTotal_prod line 726
74. def OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusWeight line 752
75. def OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusTotal line 756
76. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusTotal_prod line 759
77. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.map_inverse line 782
78. def OAI.DFVSGames.Appendix.SubspaceExtensions.subspaceEquiv line 787
79. def OAI.DFVSGames.Appendix.SubspaceExtensions.subspaceMapEquiv line 793
80. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.finrank_map_equiv line 805
81. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.weightedTotal_equiv line 808
82. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusTotal_equiv line 821
83. def OAI.DFVSGames.Appendix.SubspaceExtensions.coordinateSplit line 825
84. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusTotal_subsingleton line 839
85. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.coordinate_total_succ line 856
86. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusTotal_eq_if line 865
87. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.mobiusWeight_closed line 872
88. theorem OAI.DFVSGames.Appendix.SubspaceExtensions.binary_subspace_mobius line 881