OAI/Dynamics/StandardMap/Bernoulli/ReverseTailProjection.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.tailSigma line 13
  2. lemma OAI.HyperbolicCoding.tailSigma_le line 16
  3. lemma OAI.HyperbolicCoding.tailSigma_antitone line 21
  4. lemma OAI.HyperbolicCoding.tailEvent_of_aestronglyMeasurable line 36
  5. lemma OAI.HyperbolicCoding.ae_constant_of_trivial_thresholds line 50
  6. theorem OAI.HyperbolicCoding.tail_condExpL2_limit line 64
  7. theorem OAI.HyperbolicCoding.tail_condExpL2_constant_limit line 80
  8. def OAI.HyperbolicCoding.constL2 line 100
  9. lemma OAI.HyperbolicCoding.constL2_ae line 103
  10. lemma OAI.HyperbolicCoding.inner_constL2_one line 108
  11. theorem OAI.HyperbolicCoding.tail_condExpL2_mean_limit line 112
  12. lemma OAI.HyperbolicCoding.norm_indicatorConstLp_one_le line 133
  13. lemma OAI.HyperbolicCoding.tail_covariance_projection_bound line 139
  14. theorem OAI.HyperbolicCoding.uniform_tail_covariance_small line 164
  15. lemma OAI.HyperbolicCoding.abs_setIntegral_le_L1 line 184
  16. theorem OAI.HyperbolicCoding.uniform_tail_covariance_small_L1 line 189
  17. theorem OAI.HyperbolicCoding.ac_remote_tail_law line 231
  18. lemma OAI.HyperbolicCoding.LawClose.mono line 261
  19. def OAI.HyperbolicCoding.remotePair line 264
  20. lemma OAI.HyperbolicCoding.measurable_remotePair line 267
  21. def OAI.HyperbolicCoding.remoteProductLaw line 272
  22. def OAI.HyperbolicCoding.RemoteIndependent line 276
  23. def OAI.HyperbolicCoding.WeakBernoulliProcess line 280
  24. lemma OAI.HyperbolicCoding.stationary_tail_law line 283
  25. lemma OAI.HyperbolicCoding.ac_stationary_tail_law line 292
  26. lemma OAI.HyperbolicCoding.tail_trivial_symm line 301
  27. def OAI.HyperbolicCoding.dropName line 309
  28. lemma OAI.HyperbolicCoding.measurable_dropName line 310
  29. lemma OAI.HyperbolicCoding.stationary_drop_law line 313
  30. lemma OAI.HyperbolicCoding.measurePreserving_exchange_first line 330
  31. theorem OAI.HyperbolicCoding.product_remote_two_tail_independence line 343
  32. theorem OAI.HyperbolicCoding.local_remote_independent line 408