OAI/Computability/DirectedFeedback/Games/A4IndexCount.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Appendix.A4IndexCount.factorViaRange line 14
  2. theorem OAI.DFVSGames.Appendix.A4IndexCount.factorViaRange_apply line 21
  3. theorem OAI.DFVSGames.Appendix.A4IndexCount.factorViaRange_injective line 32
  4. theorem OAI.DFVSGames.Appendix.A4IndexCount.factorViaRange_range line 50
  5. def OAI.DFVSGames.Appendix.A4IndexCount.quotientRestriction line 67
  6. theorem OAI.DFVSGames.Appendix.A4IndexCount.ker_quotientRestriction line 70
  7. def OAI.DFVSGames.Appendix.A4IndexCount.aToRange line 76
  8. theorem OAI.DFVSGames.Appendix.A4IndexCount.aToRange_surjective line 83
  9. def OAI.DFVSGames.Appendix.A4IndexCount.encodeFixed line 91
  10. theorem OAI.DFVSGames.Appendix.A4IndexCount.encodeFixed_relation line 98
  11. theorem OAI.DFVSGames.Appendix.A4IndexCount.ker_encodeFixed line 111
  12. theorem OAI.DFVSGames.Appendix.A4IndexCount.range_encodeFixed line 119
  13. theorem OAI.DFVSGames.Appendix.A4IndexCount.recover_A0 line 127
  14. theorem OAI.DFVSGames.Appendix.A4IndexCount.recover_B0 line 140
  15. theorem OAI.DFVSGames.Appendix.A4IndexCount.encodeFixed_injective line 158
  16. def OAI.DFVSGames.Appendix.A4IndexCount.Valid line 175
  17. abbrev OAI.DFVSGames.Appendix.A4IndexCount.Index line 180
  18. abbrev OAI.DFVSGames.Appendix.A4IndexCount.GeometricIndex line 183
  19. def OAI.DFVSGames.Appendix.A4IndexCount.encode line 185
  20. theorem OAI.DFVSGames.Appendix.A4IndexCount.encode_injective line 190
  21. theorem OAI.DFVSGames.Appendix.A4IndexCount.card_index_le line 222
  22. theorem OAI.DFVSGames.Appendix.A4IndexCount.card_geometricIndex_le line 232
  23. theorem OAI.DFVSGames.Appendix.OperatorPartitions.indicator_eq_sum_of_unique_inline_OperatorPartitions line 250
  24. theorem OAI.DFVSGames.Appendix.OperatorPartitions.spectralProjector_partition line 277
  25. theorem OAI.DFVSGames.Appendix.OperatorPartitions.spectralProjector_restriction_projector line 291
  26. abbrev OAI.DFVSGames.Appendix.OperatorPartitions.A4Geometry line 311
  27. abbrev OAI.DFVSGames.Appendix.OperatorPartitions.A4GeometricIndex line 314
  28. def OAI.DFVSGames.Appendix.OperatorPartitions.a4Mask line 317
  29. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a4Mask_unique line 323
  30. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a4Mask_implies_weak line 338
  31. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a4_projector_partition line 346
  32. def OAI.DFVSGames.Appendix.OperatorPartitions.A5Geometry line 353
  33. abbrev OAI.DFVSGames.Appendix.OperatorPartitions.A5GeometricIndex line 358
  34. def OAI.DFVSGames.Appendix.OperatorPartitions.a5Mask line 362
  35. def OAI.DFVSGames.Appendix.OperatorPartitions.a5OuterMask line 367
  36. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a5Mask_unique line 374
  37. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a5Mask_implies_outer line 391
  38. theorem OAI.DFVSGames.Appendix.OperatorPartitions.a5_projector_partition line 402
  39. def OAI.DFVSGames.Appendix.RestrictionTransport.nestedEmbedding line 427
  40. theorem OAI.DFVSGames.Appendix.RestrictionTransport.nestedEmbedding_injective line 432
  41. theorem OAI.DFVSGames.Appendix.RestrictionTransport.exists_nested_embed_iff line 440
  42. theorem OAI.DFVSGames.Appendix.RestrictionTransport.nested_range_eq line 491
  43. theorem OAI.DFVSGames.Appendix.RestrictionTransport.exists_range_preimage_inline_RestrictionTransport line 508
  44. def OAI.DFVSGames.Appendix.RestrictionTransport.sameRangeEquiv line 511
  45. theorem OAI.DFVSGames.Appendix.RestrictionTransport.sameRangeEquiv_commutes line 541
  46. theorem OAI.DFVSGames.Appendix.RestrictionTransport.expect_eq_of_same_range line 549
  47. theorem OAI.DFVSGames.Appendix.RestrictionTransport.restriction_secondMoment_eq_of_same_range line 556
  48. theorem OAI.DFVSGames.Appendix.RestrictionTransport.restriction_energySquare_average_eq_of_same_range line 563
  49. theorem OAI.DFVSGames.Appendix.RestrictionTransport.nested_restriction_secondMoment_eq line 581
  50. theorem OAI.DFVSGames.Appendix.RestrictionTransport.nested_restriction_energySquare_average_eq line 597
  51. theorem OAI.DFVSGames.Appendix.LinearIdentities.a5_preimage_eq_ker line 614
  52. theorem OAI.DFVSGames.Appendix.LinearIdentities.a5_range_domRestrict_eq_of_cover line 625
  53. theorem OAI.DFVSGames.Appendix.LinearIdentities.a5_effective_annihilator line 636
  54. theorem OAI.DFVSGames.Appendix.LinearIdentities.a5_effective_codomain line 644
  55. theorem OAI.DFVSGames.Appendix.HybridComposition.effective_hybrid_iff line 683
  56. theorem OAI.DFVSGames.Appendix.HybridComposition.nested_hybridDerivative_energy line 725
  57. theorem OAI.DFVSGames.Appendix.HybridComposition.nested_hybridDerivative_energySquare_average line 754
  58. theorem OAI.DFVSGames.Appendix.HybridComposition.finrank_comap_mkQ line 767
  59. theorem OAI.DFVSGames.Appendix.HybridComposition.order_effective line 813