OAI/Computability/DirectedFeedback/Games/KMSAnalyticHybridEnergyMixed.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.mixedMapFintype line 17
  2. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound line 29
  3. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback line 49
  4. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback_iff line 60
  5. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.uniformMixedBound_of_affineDensityBound line 83
  6. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productMixedSliceBound_of_uniform line 115
  7. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.map_leftRange_complement line 155
  8. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_le_of_uniform line 167
  9. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_bound line 208
  10. def OAI.DFVSGames.Appendix.LevelInequality.IsBoolean line 228
  11. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_nonneg line 231
  12. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_sq line 235
  13. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_positive_moment line 238
  14. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_squared_norm_eq_density line 244
  15. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_four_thirds_moment line 248
  16. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_holder_fourth line 254
  17. theorem OAI.DFVSGames.Appendix.LevelInequality.fourth_power_le_implies_le line 284
  18. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_level_bound_of_fourth_moment line 291
  19. def OAI.DFVSGames.Appendix.LevelInequality.frequencyRank line 340
  20. def OAI.DFVSGames.Appendix.LevelInequality.rankLevel line 342
  21. theorem OAI.DFVSGames.Appendix.LevelInequality.linearCoeff_rankLevel line 346
  22. theorem OAI.DFVSGames.Appendix.LevelInequality.rankLevel_energy line 355
  23. theorem OAI.DFVSGames.Appendix.LevelInequality.rankLevel_inner_self line 363
  24. theorem OAI.DFVSGames.Appendix.LevelInequality.rankLevel_energy_le line 372
  25. theorem OAI.DFVSGames.Appendix.LevelInequality.rankLevel_degree_le line 379
  26. theorem OAI.DFVSGames.Appendix.LevelInequality.rankLevel_bound_of_fourth_moment line 384
  27. def OAI.DFVSGames.Appendix.LevelInequality.IsRestrictionGlobal line 395
  28. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_restriction line 401
  29. theorem OAI.DFVSGames.Appendix.LevelInequality.boolean_global_iff_density line 409
  30. def OAI.DFVSGames.Appendix.LevelInequality.Theorem23 line 418
  31. def OAI.DFVSGames.Appendix.DerivativeDegree.DegreeAtMost line 445
  32. theorem OAI.DFVSGames.Appendix.DerivativeDegree.DegreeAtMost.mono line 449
  33. theorem OAI.DFVSGames.Appendix.DerivativeDegree.degree_rankLevel line 454
  34. theorem OAI.DFVSGames.Appendix.DerivativeDegree.degree_spectralProjector line 458
  35. theorem OAI.DFVSGames.Appendix.DerivativeDegree.eq_zero_of_linearCoeff_zero line 465
  36. theorem OAI.DFVSGames.Appendix.DerivativeDegree.hybridDerivative_coeff_zero_of_lt line 484
  37. theorem OAI.DFVSGames.Appendix.DerivativeDegree.degree_hybridDerivative line 512
  38. theorem OAI.DFVSGames.Appendix.DerivativeDegree.hybridDerivative_eq_zero_of_lt_order line 519
  39. theorem OAI.DFVSGames.Appendix.DerivativeDegree.mapDerivative_coeff_zero_of_lt line 527
  40. theorem OAI.DFVSGames.Appendix.DerivativeDegree.degree_mapDerivative line 549
  41. theorem OAI.DFVSGames.Appendix.DerivativeDegree.mapDerivative_eq_zero_of_lt_rank line 555
  42. theorem OAI.DFVSGames.Appendix.DerivativeDegree.mapDerivative_zero line 562
  43. theorem OAI.DFVSGames.Appendix.DerivativeDegree.degree_map_hybridDerivative line 569
  44. theorem OAI.DFVSGames.Appendix.DerivativeDegree.map_hybridDerivative_eq_zero_of_lt_order_rank line 578
  45. theorem OAI.DFVSGames.Appendix.DerivativeDegree.map_hybridDerivative_fourth_average_eq_zero_of_lt_order_rank line 591
  46. theorem OAI.DFVSGames.Appendix.DegreeZero.rank_pos_of_ne_zero line 613
  47. theorem OAI.DFVSGames.Appendix.DegreeZero.eq_constant_of_degree_zero line 626
  48. theorem OAI.DFVSGames.Appendix.DegreeZero.fourth_moment_eq_energy_sq line 636
  49. def OAI.DFVSGames.Appendix.A5IndexCount.insideEquiv line 654
  50. theorem OAI.DFVSGames.Appendix.A5IndexCount.internal_isCompl line 663
  51. def OAI.DFVSGames.Appendix.A5IndexCount.projectionA0 line 680
  52. theorem OAI.DFVSGames.Appendix.A5IndexCount.projectionA0_injective line 686
  53. def OAI.DFVSGames.Appendix.A5IndexCount.fullRange line 716
  54. theorem OAI.DFVSGames.Appendix.A5IndexCount.fullRange_surjective line 721
  55. theorem OAI.DFVSGames.Appendix.A5IndexCount.quotientRestriction_surjective line 725
  56. theorem OAI.DFVSGames.Appendix.A5IndexCount.quotientRestriction_same_kernel line 736
  57. def OAI.DFVSGames.Appendix.A5IndexCount.sectionB0 line 750
  58. theorem OAI.DFVSGames.Appendix.A5IndexCount.range_sectionB0 line 758
  59. theorem OAI.DFVSGames.Appendix.A5IndexCount.recover_sectionB0 line 765
  60. theorem OAI.DFVSGames.Appendix.A5IndexCount.sectionB0_injective line 783
  61. def OAI.DFVSGames.Appendix.A5IndexCount.encode line 794
  62. theorem OAI.DFVSGames.Appendix.A5IndexCount.encode_injective line 800
  63. theorem OAI.DFVSGames.Appendix.A5IndexCount.card_geometricIndex_le line 813
  64. theorem OAI.DFVSGames.Appendix.A5IndexCount.card_geometricIndex_degree_le line 832
  65. theorem OAI.DFVSGames.Appendix.A5IndexCount.card_geometricIndex_cube_le line 847