OAI/Computability/DirectedFeedback/Games/KMSAnalyticHyperplaneExtensions.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.character_codomain_composition line 17
  2. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coefficient_codomain_pullback line 30
  3. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coefficient_codomain_pullback_fiber line 50
  4. def OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend line 80
  5. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_apply line 83
  6. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_comp_inl line 86
  7. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_new_coordinate line 90
  8. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_recover line 93
  9. def OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtensionEquiv line 101
  10. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_injective line 111
  11. theorem OAI.DFVSGames.Inverse.KMSAnalytic.range_hyperplaneExtend line 116
  12. theorem OAI.DFVSGames.Inverse.KMSAnalytic.range_hyperplaneExtend_of_mem line 120
  13. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ker_hyperplaneExtend_of_notMem line 125
  14. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_eq line 137
  15. theorem OAI.DFVSGames.Inverse.KMSAnalytic.card_hyperplaneExtension_outside line 148
  16. theorem OAI.DFVSGames.Inverse.KMSAnalytic.card_hyperplaneExtension_outside_pow line 155
  17. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_hyperplaneExtend_outside line 162
  18. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_hyperplaneExtend line 176
  19. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_recursion line 187
  20. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coefficient_hyperplane_restriction line 220
  21. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coefficient_zoomOut_recursion line 229
  22. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coefficient_zoomOut_mul line 241
  23. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sub_sum_sq_le_card_mul line 264
  24. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coefficient_zoomOut_sq_bound line 281
  25. def OAI.DFVSGames.Inverse.KMSAnalytic.leftEmbedding line 312
  26. theorem OAI.DFVSGames.Inverse.KMSAnalytic.leftEmbedding_injective line 315
  27. theorem OAI.DFVSGames.Inverse.KMSAnalytic.lastVector_not_mem_left_range line 321
  28. theorem OAI.DFVSGames.Inverse.KMSAnalytic.range_left_comp_of_surjective line 327
  29. def OAI.DFVSGames.Inverse.KMSAnalytic.liftedRangeEquiv line 338
  30. theorem OAI.DFVSGames.Inverse.KMSAnalytic.liftedRangeEquiv_val line 352
  31. theorem OAI.DFVSGames.Inverse.KMSAnalytic.card_lifted_range line 356
  32. theorem OAI.DFVSGames.Inverse.KMSAnalytic.sum_lifted_range line 362
  33. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_left_comp line 369
  34. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_old_injective line 390
  35. theorem OAI.DFVSGames.Inverse.KMSAnalytic.hyperplaneExtend_surjective line 397
  36. theorem OAI.DFVSGames.Inverse.KMSAnalytic.comp_hyperplaneExtend line 405
  37. theorem OAI.DFVSGames.Inverse.KMSAnalytic.dependent_extension_energy_le line 418
  38. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coefficient_lifted_zoomOut_sq_bound line 471
  39. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedCharacter_step_sum line 492
  40. def OAI.DFVSGames.Inverse.KMSAnalytic.blockFrequency line 545
  41. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockFrequency_apply line 548
  42. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockFrequency_surjective_iff line 551
  43. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ker_blockFrequency line 564
  44. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockFrequency_compatible_iff line 575
  45. def OAI.DFVSGames.Inverse.KMSAnalytic.blockOld line 592
  46. def OAI.DFVSGames.Inverse.KMSAnalytic.blockNew line 595
  47. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockOld_blockFrequency line 597
  48. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockNew_blockFrequency line 602
  49. theorem OAI.DFVSGames.Inverse.KMSAnalytic.blockFrequency_recover line 605
  50. abbrev OAI.DFVSGames.Inverse.KMSAnalytic.CompatibleBlockFrequency line 618
  51. abbrev OAI.DFVSGames.Inverse.KMSAnalytic.CompatibleOldFrequency line 623
  52. def OAI.DFVSGames.Inverse.KMSAnalytic.compatibleBlockFrequencyEquiv line 626
  53. theorem OAI.DFVSGames.Inverse.KMSAnalytic.coefficient_blockFrequency_eq line 651
  54. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_block line 668
  55. theorem OAI.DFVSGames.Inverse.KMSAnalytic.comp_blockFrequency_zero line 717
  56. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_step line 739