OAI/Computability/DirectedFeedback/Analysis/KMSMomentScalar.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.lifted_affineDensityBound line 12
  2. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_in_basis_of_tuple line 37
  3. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_shifted_basis_of_tuple line 54
  4. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.affine_expect_of_complement_of_tuple line 73
  5. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.affine_expect_bound_of_tuple line 100
  6. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.affine_squared_expect_bound_of_tuple line 117
  7. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonAffineDensity.lifted_affineDensityBound_of_tuple line 131
  8. theorem OAI.DFVSGames.Inverse.KMSMomentTheorem.lifted_fourth_moment_bound line 152
  9. def OAI.DFVSGames.Inverse.KMSMomentScalar.IsBoolean line 193
  10. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.boolean_nonneg line 196
  11. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.boolean_sq line 200
  12. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.boolean_average_nonneg line 203
  13. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.boolean_squared_average line 206
  14. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.boolean_fourth_holder line 212
  15. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.projection_energy_le_density line 240
  16. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.projection_fifth_le_density_fourth_moment line 249
  17. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.fourth_root_power line 264
  18. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.le_of_fourth_power_le line 269
  19. theorem OAI.DFVSGames.Inverse.KMSMomentScalar.lowLevel_bound_of_fourthMoment line 276
  20. def OAI.DFVSGames.Inverse.KMSLowLevel.rankEnergy line 327
  21. theorem OAI.DFVSGames.Inverse.KMSLowLevel.sum_rankEnergy line 330
  22. theorem OAI.DFVSGames.Inverse.KMSLowLevel.spectral_cutoff line 341
  23. theorem OAI.DFVSGames.Inverse.KMSLowLevel.spectral_cutoff_of_level_bounds line 363
  24. def OAI.DFVSGames.Inverse.KMSLowLevel.uniformNoise line 387
  25. theorem OAI.DFVSGames.Inverse.KMSLowLevel.uniformNoise_apply line 392
  26. theorem OAI.DFVSGames.Inverse.KMSLowLevel.uniformNoise_energy line 399
  27. theorem OAI.DFVSGames.Inverse.KMSLowLevel.rankEnergy_eq line 410
  28. theorem OAI.DFVSGames.Inverse.KMSLowLevel.rankComponent_bound line 418
  29. theorem OAI.DFVSGames.Inverse.KMSLowLevel.uniformNoise_bound_of_fourthMoments line 427
  30. theorem OAI.DFVSGames.Inverse.KMSLowLevel.projection_bound_of_general_fourthMoment line 451
  31. theorem OAI.DFVSGames.Inverse.KMSLowLevel.uniformNoise_bound_of_general_fourthMoments line 488
  32. theorem OAI.DFVSGames.Inverse.KMSLowLevel.exists_general_cutoff_parameters line 506
  33. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expect_coe_eq line 555
  34. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expect_unit_interval line 561
  35. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.mass_mul_expect line 569
  36. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expect_partition line 580
  37. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.abs_expect_sub_restrict_le line 589
  38. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.Functional line 623
  39. instance OAI.DFVSGames.Inverse.KMSBasisComparison.functionalFinite line 625
  40. instance OAI.DFVSGames.Inverse.KMSBasisComparison.functionalFintype line 629
  41. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_functional line 631
  42. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_ambient line 638
  43. def OAI.DFVSGames.Inverse.KMSBasisComparison.goodParameters line 641
  44. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.mem_goodParameters line 646
  45. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_range line 651
  46. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_goodParameters line 656
  47. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.badParameters_mass_le line 670
  48. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.badParameters_mass_le_compl line 686
  49. abbrev OAI.DFVSGames.Inverse.MatrixChart.Lines line 707
  50. abbrev OAI.DFVSGames.Inverse.MatrixChart.Hyperplanes line 710
  51. def OAI.DFVSGames.Inverse.MatrixChart.hyperplanesEquivDualLines line 713
  52. theorem OAI.DFVSGames.Inverse.MatrixChart.card_lines_binary line 730
  53. theorem OAI.DFVSGames.Inverse.MatrixChart.card_hyperplanes_binary line 762
  54. theorem OAI.DFVSGames.Inverse.MatrixChart.finrank_map_mkQ_add line 768
  55. abbrev OAI.DFVSGames.Inverse.MatrixChart.Extensions line 779
  56. def OAI.DFVSGames.Inverse.MatrixChart.extensionsEquivLines line 782
  57. theorem OAI.DFVSGames.Inverse.MatrixChart.card_extensions_binary line 802