OAI/Computability/DirectedFeedback/Games/KMSAnalyticHybridEnergyImageSplit.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.range_subtype_comp_of_surjective line 15
  2. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection line 26
  3. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_symm_val line 47
  4. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_apply_coe line 51
  5. abbrev OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency line 55
  6. abbrev OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.RankImage line 58
  7. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.frequencyImage line 61
  8. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.frequencyImageFiberEquiv line 64
  9. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv line 72
  10. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv_symm_val line 79
  11. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_fixedImage_eq_sum_surjection line 90
  12. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_rankFrequency_eq_sum_image line 99
  13. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_filter_rank_eq_sum_image line 114
  14. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_eq_sum_image_of_rank_support line 124
  15. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates line 141
  16. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_subtype line 144
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_frequency line 148
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_finrank line 156
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.exists_imageCoordinates line 161
  20. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock line 177
  21. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock_apply line 180
  22. structure OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates line 184
  23. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates.ext line 190
  24. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.assemble line 199
  25. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.assemble_apply line 203
  26. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock_assemble line 207
  27. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.extract line 216
  28. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.assemble_extract line 229
  29. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.extract_assemble line 248
  30. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.compressedFiberEquiv line 262
  31. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.assemble_injective line 271
  32. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.psi_split_inline_KMSAnalyticHybridCoordinatesConditions line 289
  33. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.hybrid_assemble_iff line 299
  34. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.fullCoordinates line 380
  35. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.embedLast line 385
  36. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.embedLast_apply line 388
  37. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.embedLast_injective line 391
  38. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.assemble_eq_embedLast_comp line 401
  39. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.range_assemble_of_fullCoordinates_surjective line 408
  40. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.finrank_assemble line 415
  41. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.ker_assemble line 422
  42. def OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.hybridFiberEquiv line 441
  43. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridCoordinates.hybridFiber_finrank line 462
  44. def OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff line 490
  45. def OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent line 494
  46. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_smallComponent line 498
  47. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_smallComponent_of_surjective line 504
  48. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coeff_smallComponent_of_not_surjective line 511
  49. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy line 518
  50. theorem OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent_smallComponent line 529
  51. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ker_comp_of_injective line 543
  52. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_eq_of_kernel_coeff_const line 549
  53. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_eq_of_kernel_coeff_const line 565
  54. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_orthogonal line 575
  55. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_le line 587
  56. def OAI.DFVSGames.Inverse.KMSKernelOrbits.rangeEquivOfKerEq line 617
  57. theorem OAI.DFVSGames.Inverse.KMSKernelOrbits.rangeEquivOfKerEq_apply line 622
  58. theorem OAI.DFVSGames.Inverse.KMSKernelOrbits.exists_postcomp_equiv_of_ker_eq line 631
  59. theorem OAI.DFVSGames.Inverse.KMSKernelOrbits.ker_eq_iff_exists_postcomp_equiv line 641
  60. def OAI.DFVSGames.Inverse.KMSBasisInvariant.primalChange line 662
  61. def OAI.DFVSGames.Inverse.KMSBasisInvariant.frequencyChange line 668
  62. def OAI.DFVSGames.Inverse.KMSBasisInvariant.IsBasisInvariant line 674
  63. theorem OAI.DFVSGames.Inverse.KMSBasisInvariant.character_change line 677
  64. theorem OAI.DFVSGames.Inverse.KMSBasisInvariant.coefficient_change line 685
  65. def OAI.DFVSGames.Inverse.KMSBasisInvariant.frequencyRank line 695
  66. theorem OAI.DFVSGames.Inverse.KMSBasisInvariant.frequencyRank_change line 698
  67. def OAI.DFVSGames.Inverse.KMSBasisInvariant.rankProjection line 705
  68. theorem OAI.DFVSGames.Inverse.KMSBasisInvariant.rankProjection_invariant line 708