OAI/Computability/DirectedFeedback/Games/Derivatives.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Appendix.Derivatives.spectralProjector line 17
  2. theorem OAI.DFVSGames.Appendix.Derivatives.linearCoeff_spectralProjector line 21
  3. theorem OAI.DFVSGames.Appendix.Derivatives.spectralProjector_energy line 30
  4. theorem OAI.DFVSGames.Appendix.Derivatives.spectralProjector_energy_le line 40
  5. theorem OAI.DFVSGames.Appendix.Derivatives.function_eq_of_linearCoeff_eq line 48
  6. theorem OAI.DFVSGames.Appendix.Derivatives.spectralProjector_comp line 56
  7. def OAI.DFVSGames.Appendix.Derivatives.hybridProjector line 66
  8. def OAI.DFVSGames.Appendix.Derivatives.hybridDerivative line 70
  9. def OAI.DFVSGames.Appendix.Derivatives.rankProjector line 75
  10. def OAI.DFVSGames.Appendix.Derivatives.mapDerivative line 79
  11. theorem OAI.DFVSGames.Appendix.Derivatives.rankProjector_energy line 83
  12. def OAI.DFVSGames.Appendix.Derivatives.selectorMultiplicity line 90
  13. theorem OAI.DFVSGames.Appendix.Derivatives.selector_energy_sum line 94
  14. theorem OAI.DFVSGames.Appendix.Derivatives.selector_energy_sum_le line 108
  15. theorem OAI.DFVSGames.Appendix.Derivatives.linearCoeff_mapDerivative line 123
  16. theorem OAI.DFVSGames.Appendix.Derivatives.mapDerivative_energy_eq_coefficients line 141
  17. theorem OAI.DFVSGames.Appendix.Derivatives.mapDerivative_energy_le line 151
  18. theorem OAI.DFVSGames.Appendix.Derivatives.mapDerivative_energy_eq_weighted_energy line 165
  19. theorem OAI.DFVSGames.Appendix.Derivatives.weighted_fourth_derivative_energy line 174
  20. theorem OAI.DFVSGames.Appendix.Derivatives.spectralProjector_restriction line 189
  21. theorem OAI.DFVSGames.Appendix.Derivatives.spectralProjector_restriction_moment_average line 214
  22. theorem OAI.DFVSGames.Appendix.Derivatives.hybridDerivative_energy_average line 229
  23. def OAI.DFVSGames.Appendix.Derivatives.HybridIndex line 236
  24. instance OAI.DFVSGames.Appendix.Derivatives.hybridIndexFintype line 240
  25. def OAI.DFVSGames.Appendix.Derivatives.hybridMomentSum line 249
  26. def OAI.DFVSGames.Appendix.Derivatives.hybridSelectorEnergy line 253
  27. theorem OAI.DFVSGames.Appendix.Derivatives.hybridMomentSum_le_of_uniform_energy line 258
  28. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative line 302
  29. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_eq_coefficients line 319
  30. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv line 339
  31. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv_coe line 350
  32. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.quotientRightMap line 353
  33. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.quotientRightMap_mkQ line 359
  34. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv line 363
  35. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv_mkQ line 382
  36. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv line 386
  37. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_compressFrequency line 414
  38. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.compressFrequency_eq_iff_product line 426
  39. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_product_energy_eq_coefficients line 445
  40. def OAI.DFVSGames.Inverse.KMSAnalytic.synthesis line 481
  41. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_synthesis line 484
  42. theorem OAI.DFVSGames.Inverse.KMSAnalytic.synthesis_coeff line 491
  43. theorem OAI.DFVSGames.Inverse.KMSAnalytic.eq_of_coeff_eq line 496
  44. theorem OAI.DFVSGames.Inverse.KMSAnalytic.synthesis_inner line 501
  45. theorem OAI.DFVSGames.Inverse.KMSAnalytic.synthesis_energy line 506
  46. def OAI.DFVSGames.Inverse.KMSAnalytic.component line 511
  47. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_component line 515
  48. theorem OAI.DFVSGames.Inverse.KMSAnalytic.component_energy line 520
  49. theorem OAI.DFVSGames.Inverse.KMSAnalytic.component_energy_le line 528
  50. theorem OAI.DFVSGames.Inverse.KMSAnalytic.component_inner_self line 535
  51. theorem OAI.DFVSGames.Inverse.KMSAnalytic.component_comp line 544
  52. theorem OAI.DFVSGames.Inverse.KMSAnalytic.component_orthogonal line 552
  53. def OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent line 564
  54. theorem OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent_energy line 567
  55. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybrid_frequency_rank line 598
  56. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative_rankComponent_eq_zero line 612
  57. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_eq_zero_of_lt_order line 631
  58. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_support line 642
  59. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank line 657
  60. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank_fibers line 673
  61. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_finrank line 694
  62. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.product_restriction_order line 706
  63. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_product_energy_eq_rank_fibers line 718