OAI/Computability/DirectedFeedback/Games/NaturalTransport.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Appendix.OperatorNorm.energy_sum_sq_le_card_cube line 18
  2. theorem OAI.DFVSGames.Appendix.OperatorNorm.fourth_sum_le_card_cube line 53
  3. theorem OAI.DFVSGames.Appendix.OperatorNorm.average_fourth_sum_le_card_cube line 58
  4. theorem OAI.DFVSGames.Appendix.OperatorNorm.compressFrequency_eq_compress line 87
  5. theorem OAI.DFVSGames.Appendix.OperatorNorm.nested_projector_restriction_apply line 92
  6. theorem OAI.DFVSGames.Appendix.OperatorNorm.a5_outer_energy line 112
  7. theorem OAI.DFVSGames.Appendix.OperatorNorm.a5_summand_energy line 162
  8. theorem OAI.DFVSGames.Appendix.OperatorNorm.a5_energySquare_le line 214
  9. theorem OAI.DFVSGames.Appendix.OperatorNorm.map_hybrid_fourth_average line 259
  10. theorem OAI.DFVSGames.Appendix.OperatorNorm.a4_fourth_average_le line 283
  11. theorem OAI.DFVSGames.Appendix.NaturalTransport.rank_arrowCongr line 344
  12. theorem OAI.DFVSGames.Appendix.NaturalTransport.rankBelow_arrowCongr line 355
  13. theorem OAI.DFVSGames.Appendix.NaturalTransport.trace_arrowCongr line 363
  14. theorem OAI.DFVSGames.Appendix.NaturalTransport.character_arrowCongr line 372
  15. theorem OAI.DFVSGames.Appendix.NaturalTransport.admissible_arrowCongr line 379
  16. theorem OAI.DFVSGames.Appendix.NaturalTransport.derivative_embedding_range line 387
  17. theorem OAI.DFVSGames.Appendix.NaturalTransport.linearCoeff_pullback line 422
  18. theorem OAI.DFVSGames.Appendix.NaturalTransport.rankProjector_pullback line 435
  19. theorem OAI.DFVSGames.Appendix.NaturalTransport.mapDerivative_energy_pullback line 447
  20. def OAI.DFVSGames.Appendix.NaturalTransport.quotientFactor line 468
  21. theorem OAI.DFVSGames.Appendix.NaturalTransport.quotientFactor_mkQ line 476
  22. def OAI.DFVSGames.Appendix.NaturalTransport.outputFactor line 481
  23. theorem OAI.DFVSGames.Appendix.NaturalTransport.outputFactor_val line 486
  24. def OAI.DFVSGames.Appendix.NaturalTransport.parameterFactor line 489
  25. def OAI.DFVSGames.Appendix.NaturalTransport.dualFactor line 494
  26. theorem OAI.DFVSGames.Appendix.NaturalTransport.dualFactor_rank line 502
  27. theorem OAI.DFVSGames.Appendix.NaturalTransport.parameterFactor_embedding line 510
  28. theorem OAI.DFVSGames.Appendix.NaturalTransport.nested_hybridDerivative_function line 520
  29. theorem OAI.DFVSGames.Appendix.NaturalTransport.nested_mapDerivative_energy line 543
  30. theorem OAI.DFVSGames.Appendix.NaturalTransport.nested_mapDerivative_energySquare_average line 555
  31. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.mem_map_equiv_iff_inline_KMSAnalyticHybridEnergyTransport line 587
  32. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybrid_arrowCongr line 597
  33. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.restriction_admissible_arrowCongr line 628
  34. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybrid_embedding_range line 658
  35. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridProjector_pullback line 689
  36. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.rankComponent_pullback line 699
  37. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_pullback line 710
  38. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_pullback line 727
  39. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv line 756
  40. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imagePullback line 760
  41. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageTranslate line 765
  42. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv_leftRange line 770
  43. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_hybrid_iff line 781
  44. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_compression_eq_iff line 801
  45. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_character line 829
  46. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_rank_coefficient line 839
  47. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_coefficient_sum_transport line 851