OAI/Computability/DirectedFeedback/Games/CoordinateTransport.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Appendix.CoordinateTransport.complementRangeEquiv line 13
  2. theorem OAI.DFVSGames.Appendix.CoordinateTransport.complementRangeEquiv_apply line 17
  3. def OAI.DFVSGames.Appendix.CoordinateTransport.domainEquiv line 22
  4. theorem OAI.DFVSGames.Appendix.CoordinateTransport.apply_domainEquiv line 27
  5. def OAI.DFVSGames.Appendix.CoordinateTransport.codomainEquiv line 36
  6. theorem OAI.DFVSGames.Appendix.CoordinateTransport.canonical_block line 40
  7. theorem OAI.DFVSGames.Appendix.CoordinateTransport.exists_canonical_coordinates line 47
  8. theorem OAI.DFVSGames.Appendix.CoordinateTransport.domainEquiv_zero_left line 56
  9. theorem OAI.DFVSGames.Appendix.CoordinateTransport.quotient_coordinates line 62
  10. def OAI.DFVSGames.Appendix.CoordinateTransport.toBlocks line 68
  11. theorem OAI.DFVSGames.Appendix.CoordinateTransport.toBlocks_apply line 73
  12. theorem OAI.DFVSGames.Appendix.CoordinateTransport.compressed_toBlocks line 80
  13. theorem OAI.DFVSGames.Appendix.CoordinateTransport.toBlocks_base line 87
  14. def OAI.DFVSGames.Appendix.CoordinateTransport.rangeTransport line 100
  15. theorem OAI.DFVSGames.Appendix.CoordinateTransport.finrank_range_transport line 115
  16. theorem OAI.DFVSGames.Appendix.CoordinateTransport.finrank_toBlocks line 123
  17. theorem OAI.DFVSGames.Appendix.CoordinateTransport.finrank_comp_equiv line 129
  18. def OAI.DFVSGames.Appendix.FullCompression.compression line 151
  19. theorem OAI.DFVSGames.Appendix.FullCompression.compression_apply line 155
  20. def OAI.DFVSGames.Appendix.FullCompression.Fiber line 158
  21. theorem OAI.DFVSGames.Appendix.FullCompression.fiber_condition_iff line 163
  22. def OAI.DFVSGames.Appendix.FullCompression.fiberEquiv line 199
  23. theorem OAI.DFVSGames.Appendix.FullCompression.card_fiber line 208
  24. theorem OAI.DFVSGames.Appendix.FullCompression.fiber_rank line 216
  25. theorem OAI.DFVSGames.Appendix.FiberEnergy.finite_fiber_energy line 241
  26. theorem OAI.DFVSGames.Appendix.DerivativeEnergy.supported_fiber_energy line 280
  27. theorem OAI.DFVSGames.Appendix.DerivativeEnergy.coefficient_energy line 326
  28. def OAI.DFVSGames.Appendix.SubspaceCounting.generators line 370
  29. theorem OAI.DFVSGames.Appendix.SubspaceCounting.span_generators line 374
  30. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_subspaces_rank_le line 381
  31. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_subspaces_rank_le_field_power line 396
  32. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_binary_subspaces_rank_le line 404
  33. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_linearMaps_le line 419
  34. theorem OAI.DFVSGames.Appendix.SubspaceCounting.exists_rank_factorization line 431
  35. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_rank_maps_le line 440
  36. def OAI.DFVSGames.Appendix.SubspaceCounting.quotientImageMap line 478
  37. theorem OAI.DFVSGames.Appendix.SubspaceCounting.quotientImageMap_mk line 488
  38. theorem OAI.DFVSGames.Appendix.SubspaceCounting.rank_quotientImageMap line 494
  39. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_constrained_maps_le line 505
  40. theorem OAI.DFVSGames.Appendix.SubspaceCounting.binary_add_cancel line 549
  41. theorem OAI.DFVSGames.Appendix.SubspaceCounting.card_binary_predecessors_le line 557
  42. lemma OAI.DFVSGames.Appendix.WeightedFourthMoment.half_cancel_inline_WeightedFourthMoment line 614
  43. lemma OAI.DFVSGames.Appendix.WeightedFourthMoment.half_sum_identity_inline_WeightedFourthMoment line 619
  44. lemma OAI.DFVSGames.Appendix.WeightedFourthMoment.half_sum_le_inline_WeightedFourthMoment line 628
  45. lemma OAI.DFVSGames.Appendix.WeightedFourthMoment.finite_level_sum_inline_WeightedFourthMoment line 634
  46. abbrev OAI.DFVSGames.Appendix.WeightedFourthMoment.rank line 691
  47. def OAI.DFVSGames.Appendix.WeightedFourthMoment.vectorFintype line 693
  48. def OAI.DFVSGames.Appendix.WeightedFourthMoment.compressedFintype line 697
  49. def OAI.DFVSGames.Appendix.WeightedFourthMoment.energy line 703
  50. theorem OAI.DFVSGames.Appendix.WeightedFourthMoment.predecessor_weight_sum line 709
  51. theorem OAI.DFVSGames.Appendix.WeightedFourthMoment.weighted_fourth_coefficient_energy line 737