OAI/Computability/DirectedFeedback/Games/KMSAnalyticSmallTransport.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSAnalytic.smallFrequencyEquiv line 19
  2. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallFrequencyEquiv_apply line 25
  3. theorem OAI.DFVSGames.Inverse.KMSAnalytic.surjective_smallFrequencyEquiv_iff line 28
  4. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallFrequency_transport_comp line 40
  5. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_transport line 54
  6. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_transport line 63
  7. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_transport line 79
  8. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_precomp_equiv line 91
  9. def OAI.DFVSGames.Inverse.KMSPointComplement.pointEquivOfIsCompl line 109
  10. theorem OAI.DFVSGames.Inverse.KMSPointComplement.pointEquivOfIsCompl_apply line 115
  11. theorem OAI.DFVSGames.Inverse.KMSPointComplement.exists_aligned_point_equiv line 119
  12. theorem OAI.DFVSGames.Inverse.KMSPointComplement.exists_point_equiv line 150
  13. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.exists_mixed_aligned_point line 174
  14. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.smallComponent_mixed_aligned line 197
  15. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_smallComponent_mixed_aligned line 220
  16. def OAI.DFVSGames.Inverse.KMSFourthMoment.zeroFixedEquiv line 247
  17. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.zeroFixedEquiv_apply line 255
  18. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.zeroFixedEquiv_symm_apply line 258
  19. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_smallComponent_zeroFixed line 274
  20. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixedEnergy_zeroFixed line 291
  21. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le line 324
  22. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le_of_bounds line 347
  23. def OAI.DFVSGames.Inverse.KMSFourthMoment.mixedStepFactor line 378
  24. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixedStepFactor_nonneg line 380
  25. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.one_le_mixedStepFactor line 384
  26. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_step_factor_bound line 387
  27. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_weighted_step line 402
  28. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_weighted_step_pow line 415
  29. def OAI.DFVSGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound line 452
  30. theorem OAI.DFVSGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_pullback line 459
  31. theorem OAI.DFVSGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.energy_le line 470
  32. theorem OAI.DFVSGames.Inverse.KMSAnalytic.basisInvariant_codomain_pullback line 477
  33. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointAppend_comp_basis line 495
  34. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointRestrict_invariant line 502
  35. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointAppend_add line 510
  36. theorem OAI.DFVSGames.Inverse.KMSAnalytic.pointRestrict_translate line 526
  37. def OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound line 549
  38. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound.mono line 560
  39. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound.homogeneous line 566
  40. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound.pointRestrict line 574
  41. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound.domain_equiv line 613
  42. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.AffineDensityBound.codomain_pullback line 627
  43. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.mixed_bound_of_character_bound line 663