OAI/Computability/DirectedFeedback/Probability/KMSMomentConstants.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Appendix.HybridCounting.comap_subtype_injective_inline_HybridCounting line 11
  2. theorem OAI.DFVSGames.Appendix.HybridCounting.map_quotient_injective_inline_HybridCounting line 24
  3. theorem OAI.DFVSGames.Appendix.HybridCounting.finite_submodules_inline_HybridCounting line 42
  4. theorem OAI.DFVSGames.Appendix.HybridCounting.card_hybrid_pairs_le line 51
  5. theorem OAI.DFVSGames.Appendix.HybridCounting.card_hybridIndex_le_two line 94
  6. theorem OAI.DFVSGames.Appendix.HybridCounting.card_hybridIndex_le line 113
  7. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.selector_energy_le line 139
  8. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.fourth_moment_le_of_uniform_hybrid_energy line 158
  9. theorem OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent_eq_rankProjection line 200
  10. theorem OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent_invariant line 210
  11. theorem OAI.DFVSGames.Inverse.KMSAnalytic.rankComponent_coeff_eq_zero_of_ne line 215
  12. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.rankComponent_degree line 237
  13. theorem OAI.DFVSGames.Inverse.KMSFourthMoment.rankComponent_fourth_moment_le_of_hybrid line 245
  14. def OAI.DFVSGames.Inverse.KMSMomentConstants.fourthMomentConstant line 262
  15. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.fourthMomentConstant_pos line 264
  16. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.fourthMomentConstant_nonneg line 268
  17. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.mixedRankConstant_eq line 271
  18. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.a5_mul_mixedRankConstant line 278
  19. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.fourthMomentConstant_mono line 285
  20. theorem OAI.DFVSGames.Inverse.KMSMomentConstants.a5_mixed_bound line 293
  21. def OAI.DFVSGames.Inverse.KMS.relativeDensity line 317
  22. theorem OAI.DFVSGames.Inverse.KMS.inter_chart_eq line 320
  23. theorem OAI.DFVSGames.Inverse.KMS.chart_inter_nonempty line 330
  24. theorem OAI.DFVSGames.Inverse.KMS.relativeDensity_le_chart line 336
  25. theorem OAI.DFVSGames.Inverse.KMS.density_bound_passes_to_chart line 345
  26. abbrev OAI.DFVSGames.Inverse.KMS.F2 line 353
  27. abbrev OAI.DFVSGames.Inverse.KMS.Ambient line 354
  28. def OAI.DFVSGames.Inverse.KMS.Vertex line 356
  29. instance OAI.DFVSGames.Inverse.KMS.vertexFinite line 359
  30. instance OAI.DFVSGames.Inverse.KMS.vertexFintype line 366
  31. def OAI.DFVSGames.Inverse.KMS.Adjacent line 368
  32. def OAI.DFVSGames.Inverse.KMS.neighbors line 371
  33. def OAI.DFVSGames.Inverse.KMS.retention line 374
  34. def OAI.DFVSGames.Inverse.KMS.interval line 377
  35. def OAI.DFVSGames.Inverse.KMS.ExpansionPrinciple line 381
  36. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.BasisMap line 399
  37. instance OAI.DFVSGames.Inverse.KMSBasisComparison.basisMapFinite line 401
  38. instance OAI.DFVSGames.Inverse.KMSBasisComparison.basisMapFintype line 405
  39. def OAI.DFVSGames.Inverse.KMSBasisComparison.InLift line 407
  40. def OAI.DFVSGames.Inverse.KMSBasisComparison.lift line 410
  41. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.mem_lift line 413
  42. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftedIndicator line 417
  43. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftedIndicator_nonneg line 420
  44. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftedIndicator_le_one line 425
  45. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.injective_of_inLift line 430
  46. def OAI.DFVSGames.Inverse.KMSBasisComparison.rangeVertex line 442
  47. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.inLift_iff_rangeVertex_mem line 448
  48. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.inLift_comp_iff line 458
  49. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftedIndicator_basisInvariant line 464
  50. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.nat_card_eq_sum_fibers line 479
  51. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.nat_card_event_eq_sum_fibers line 483
  52. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.uniformFiber_card_ratio line 494
  53. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.subtype_event_ratio_le line 510
  54. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.exists_restricted_completion line 535
  55. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.RestrictedCompletion line 608
  56. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionBasis line 615
  57. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionBasis_coe line 619
  58. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionOfBasis line 624
  59. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv line 645
  60. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_basis line 650
  61. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_symm line 656
  62. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_sub_mem line 662
  63. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionSpanEquiv_mem_iff line 682
  64. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion line 693
  65. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_coe line 711
  66. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.transportCompletion_inverse line 718
  67. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionEquiv line 734
  68. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedCompletionCard_eq line 743