OAI/Computability/DirectedFeedback/Games/KMSKernelFiberDefs.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_comp_eq_fiber_card line 15
  2. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_sq_eq_fiber_card line 30
  3. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_sq_eq_uniform_fiber_card line 36
  4. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fiber_constant_energy_cross_mul line 45
  5. theorem OAI.DFVSGames.Inverse.KMSAnalytic.synthesis_energy_grouped line 76
  6. theorem OAI.DFVSGames.Inverse.KMSAnalytic.synthesis_energy_by_kernel line 83
  7. abbrev OAI.DFVSGames.Inverse.KMSKernelFiberCard.F2 line 98
  8. abbrev OAI.DFVSGames.Inverse.KMSKernelFiberCard.KernelClass line 105
  9. abbrev OAI.DFVSGames.Inverse.KMSKernelFiberCard.RankFrequency line 108
  10. abbrev OAI.DFVSGames.Inverse.KMSKernelFiberCard.FullFrequency line 111
  11. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.rankKernel line 115
  12. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.fullKernel line 118
  13. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.rankKernel_val line 121
  14. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.fullKernel_val line 124
  15. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.ker_comp_mkQ line 137
  16. def OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection line 142
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_apply_mkQ line 159
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_symm_apply line 164
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.range_forward line 168
  20. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.finrank_range_forward line 173
  21. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.fixedKernel_finrank_eq_quotient line 179
  22. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.range_comp_mkQ line 185
  23. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.quotientInjection_comp_finrank line 195
  24. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.natCard_fixedKernel_eq_injectiveQuotient line 201
  25. theorem OAI.DFVSGames.Inverse.KMSAnalyticKernelCount.card_fixedKernel_eq_injectiveQuotient line 206
  26. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.quotientEquiv line 227
  27. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.rankKernel_surjective line 230
  28. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.fullKernel_surjective line 244
  29. abbrev OAI.DFVSGames.Inverse.KMSInjectionCount.F2 line 264
  30. def OAI.DFVSGames.Inverse.KMSInjectionCount.beta line 269
  31. def OAI.DFVSGames.Inverse.KMSInjectionCount.injectiveEquivIndependent line 271
  32. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_eq_product line 284
  33. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.injectionEquivOfDomainEquiv line 309
  34. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.fixedKernelEquivInjection line 329
  35. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.natCard_fixedKernel_eq_beta line 335
  36. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.rankFiberEquivFixedKernel line 339
  37. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.surjective_of_kernel_class line 356
  38. def OAI.DFVSGames.Inverse.KMSKernelFiberCard.fullFiberEquivFixedKernel line 362
  39. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.rankKernel_fiber_card line 376
  40. theorem OAI.DFVSGames.Inverse.KMSKernelFiberCard.fullKernel_fiber_card line 389
  41. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.binary_factor_lower line 409
  42. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_le_pow line 425
  43. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_ge_pow line 435
  44. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_positive line 448
  45. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_self_le line 452
  46. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_cross_mul line 483
  47. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_ratio line 511
  48. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_pow_bound line 528
  49. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_le_of_energy_le line 554
  50. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.pow_dim_mul_le_pow_sq_mul_beta line 576
  51. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.beta_ratio_le_pow line 593
  52. theorem OAI.DFVSGames.Inverse.KMSInjectionCount.pow_mul_le_of_beta_cross_mul line 619
  53. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_energy_base_bound line 665
  54. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero_dim_bound line 691