OAI/Computability/DirectedFeedback/Games/KMSAnalyticCodomainTransport.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedCharacter_constant_step line 9
  2. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_bound line 95
  3. def OAI.DFVSGames.Inverse.KMSAnalytic.codomainTransport line 213
  4. def OAI.DFVSGames.Inverse.KMSAnalytic.codomainFrequencyEquiv line 216
  5. theorem OAI.DFVSGames.Inverse.KMSAnalytic.codomainFrequencyEquiv_apply line 222
  6. theorem OAI.DFVSGames.Inverse.KMSAnalytic.codomainFrequency_cancel line 225
  7. theorem OAI.DFVSGames.Inverse.KMSAnalytic.surjective_comp_codomainEquiv_iff line 228
  8. theorem OAI.DFVSGames.Inverse.KMSAnalytic.linearCoeff_codomainTransport line 244
  9. theorem OAI.DFVSGames.Inverse.KMSAnalytic.basisInvariant_codomainTransport line 264
  10. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_codomainTransport line 279
  11. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_codomainTransport line 290
  12. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_codomainTransport line 301
  13. theorem OAI.DFVSGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.mono line 333
  14. theorem OAI.DFVSGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_equiv line 339
  15. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_postcomp_injective line 357
  16. def OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv line 381
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_snd line 410
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_fst_coe line 413
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply line 416
  20. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply_zero line 420
  21. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_ker line 424
  22. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_unit line 429
  23. theorem OAI.DFVSGames.Inverse.KMSAnalyticFunctionalSplit.finrank_eq_ker_add_one line 434
  24. abbrev OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.F2 line 446
  25. structure OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting line 453
  26. abbrev OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.K0 line 468
  27. abbrev OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.J line 469
  28. abbrev OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.B line 470
  29. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv line 472
  30. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv line 476
  31. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv line 481
  32. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap line 486
  33. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap line 490
  34. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_apply_val line 494
  35. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_apply_val line 497
  36. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_surjective line 500
  37. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_surjective line 511
  38. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv_symm_apply line 522
  39. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv_symm_apply line 525
  40. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv_symm_apply line 528
  41. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_symm_apply line 531
  42. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_symm_apply line 536
  43. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_conjugation line 541
  44. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_conjugation line 549
  45. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.target_finrank line 557
  46. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_finrank line 562
  47. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_finrank line 568
  48. theorem OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.exists_compatibleSplitting line 576
  49. def OAI.DFVSGames.Inverse.KMSAnalyticCompatibleSplitting.chooseSplit line 588
  50. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_bound_induction_inline_KMSAnalyticCharacterInduction line 614
  51. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_le_of_homogeneous line 687
  52. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_slice_bound line 723
  53. def OAI.DFVSGames.Inverse.KMSFourthMoment.mixedRankConstant line 744
  54. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixedRankConstant_nonneg line 746
  55. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_slice_bound_uniform line 750