OAI/Computability/DirectedFeedback/Games/KMSAnalyticHybridEnergyFiber.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSKernelOrbitsFourier.coefficient_eq_of_ker_eq line 19
  2. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_eq_of_basisInvariant line 47
  3. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_eq_of_basisInvariant line 56
  4. theorem OAI.DFVSGames.Inverse.KMSAnalytic.surjective_postcomp_equiv line 64
  5. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_postcomp_equiv line 77
  6. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_invariant line 91
  7. abbrev OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.Extension line 120
  8. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.coordinatesDataEquiv line 123
  9. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.compressedFiberDataEquiv line 131
  10. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.extensionEquiv line 137
  11. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybrid_rank_coeff_assemble line 161
  12. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.tracePair_prod line 207
  13. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod line 222
  14. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_re line 229
  15. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_coprod_re line 237
  16. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble line 251
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_re line 262
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates line 273
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates_re line 281
  20. def OAI.DFVSGames.Inverse.KMSAnalytic.pointAppend line 301
  21. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointAppend_apply line 304
  22. def OAI.DFVSGames.Inverse.KMSAnalytic.pointRestrict line 307
  23. def OAI.DFVSGames.Inverse.KMSAnalytic.pointLift line 310
  24. def OAI.DFVSGames.Inverse.KMSAnalytic.pointPad line 313
  25. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointLift_injective line 316
  26. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointPad_injective line 323
  27. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointLift_comp_prod line 328
  28. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointPad_comp line 333
  29. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ker_le_of_not_surjective_prod line 336
  30. theorem OAI.DFVSGames.Inverse.KMSAnalytic.not_surjective_prod_iff line 355
  31. theorem OAI.DFVSGames.Inverse.KMSAnalytic.surjective_of_surjective_prod line 380
  32. def OAI.DFVSGames.Inverse.KMSAnalytic.dependentRowEquiv line 387
  33. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ker_prod_pullback line 407
  34. def OAI.DFVSGames.Inverse.KMSAnalytic.frequencyProdEquiv line 429
  35. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_frequency_prod line 437
  36. theorem OAI.DFVSGames.Inverse.KMSAnalytic.tracePair_pointAppend line 448
  37. theorem OAI.DFVSGames.Inverse.KMSAnalytic.character_pointAppend line 459
  38. theorem OAI.DFVSGames.Inverse.KMSAnalytic.tracePair_pointShift line 467
  39. theorem OAI.DFVSGames.Inverse.KMSAnalytic.character_pointShift line 478
  40. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointRestrict_eq_synthesis line 491
  41. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_pointRestrict line 506
  42. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_dependentRows line 526
  43. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_rows_split line 538
  44. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_dependent_extension line 555
  45. theorem OAI.DFVSGames.Inverse.KMSAnalytic.point_row_recursion line 576
  46. theorem OAI.DFVSGames.Inverse.KMSAnalytic.point_restriction_recursion_add line 617
  47. theorem OAI.DFVSGames.Inverse.KMSAnalytic.point_restriction_recursion line 640
  48. def OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy line 664
  49. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_nonneg line 668
  50. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coeff_translate line 672
  51. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_translate line 689
  52. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_sub_sum_le line 703
  53. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_sub_translates_le line 734