OAI/Computability/DirectedFeedback/Probability/KMSFourthMomentMixedRestriction.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict line 17
  2. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_apply line 20
  3. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coprod_add_shift line 24
  4. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_translate line 39
  5. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_sub_sum line 51
  6. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_translate line 60
  7. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_sub_translates_le line 68
  8. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.frequencyBlockEquiv line 100
  9. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_frequency_blocks line 108
  10. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.partialRestrict_eq_synthesis line 124
  11. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.coeff_partialRestrict line 141
  12. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.coordinateOfData line 165
  13. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.primalA line 170
  14. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.primalW line 173
  15. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.primalD line 176
  16. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_compressedFiber line 182
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_alpha_hybrid_term line 208
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.hybrid_fiber_coefficient_factorization line 240
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.phase_weighted_sum_sq_le line 281
  20. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.phase_sum_sq_le_card_sq line 291
  21. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_fiber_phase_sq_le line 299
  22. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_fiber_product_sq_le line 321
  23. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber_eq line 351
  24. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.natCard_extension line 368
  25. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber line 374
  26. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.card_linearMap_eq line 390
  27. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.natCard_injective_le line 396
  28. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.card_injective_le line 410
  29. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.natCard_rank_subspaces_le line 421
  30. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.card_rank_subspaces_le line 428
  31. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.count_exponent_le line 435
  32. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.count_budget_le line 442
  33. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.count_budget_le_of_dimension line 463
  34. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_fixed_snd line 498
  35. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_snd_eq_sum line 530
  36. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sum_extensions_eq_filter line 544
  37. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient line 579
  38. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.traceCharacter_re_sq line 591
  39. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_mixed line 598
  40. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_of_mixed line 656