OAI/Computability/DirectedFeedback/Probability/KMSFourthMomentZoomTransport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.image_fiber_coefficient_transport line 23
  2. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.basisInvariant_pullback line 75
  3. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.surjective_comp_symm_iff_inline_KMSAnalyticHybridEnergyTransportSmall line 90
  4. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.smallCoeff_pullback line 111
  5. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback line 128
  6. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback_apply line 149
  7. def OAI.DFVSGames.Inverse.KMSAnalytic.ambientPrimalEquiv line 170
  8. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ambient_character_transport line 177
  9. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ambient_basisInvariant_transport line 183
  10. theorem OAI.DFVSGames.Inverse.KMSAnalytic.ambient_coeff_transport line 199
  11. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallCoeff_ambient_transport line 216
  12. theorem OAI.DFVSGames.Inverse.KMSAnalytic.smallComponent_ambient_transport line 227
  13. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound line 270
  14. def OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient line 286
  15. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient_imageTransport line 295
  16. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.product_energy_eq_filter_coefficient line 305
  17. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.product_image_energy_le_of_mixed line 323
  18. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.product_hybrid_energy_le_of_mixed line 397
  19. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.partialRestrict_codomain_pullback line 495
  20. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_left_apply_inline_KMSAnalyticHybridEnergyTransportSmallMixed line 508
  21. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_right_apply_inline_KMSAnalyticHybridEnergyTransportSmallMixed line 513
  22. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_postcomp_equiv line 526
  23. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_codomain_pullback line 534
  24. theorem OAI.DFVSGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_partialRestrict_smallComponent_pullback line 565
  25. def OAI.DFVSGames.Inverse.KMSFourthMoment.pointShuffle line 595
  26. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.pointShuffle_apply line 617
  27. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.pointShuffle_symm_apply line 621
  28. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.coprod_comp_pointShuffle line 626
  29. def OAI.DFVSGames.Inverse.KMSFourthMoment.pointShuffleTransport line 644
  30. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.partialRestrict_pointRestrict_pointShuffleTransport line 649
  31. def OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy line 685
  32. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_nonneg line 690
  33. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq line 697
  34. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_zero_of_not_surjective line 711
  35. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_le line 724
  36. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero line 733
  37. theorem OAI.DFVSGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_of_basisInvariant line 742