OAI/Dynamics/MultipleMixing/Main.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Rokhlin.Spaced line 14
  2. def OAI.Rokhlin.SequentialMixing line 17
  3. lemma OAI.Rokhlin.proper_rectangles_of_induction line 22
  4. lemma OAI.Rokhlin.sequential_zero line 42
  5. lemma OAI.Rokhlin.sequential_one line 47
  6. lemma OAI.Rokhlin.shifted_pair line 58
  7. lemma OAI.Rokhlin.sequential_two line 67
  8. def OAI.Rokhlin.setIndicator line 92
  9. lemma OAI.Rokhlin.setIndicator_bounds line 94
  10. lemma OAI.Rokhlin.setIndicator_measurable line 98
  11. lemma OAI.Rokhlin.prod_setIndicator line 101
  12. lemma OAI.Rokhlin.integral_setIndicator line 112
  13. lemma OAI.Rokhlin.integral_prod_setIndicator line 119
  14. lemma OAI.Rokhlin.setIndicator_preimage line 124
  15. lemma OAI.Rokhlin.sequential_step line 135
  16. theorem OAI.Rokhlin.sequential_mixing_all line 227
  17. lemma OAI.Rokhlin.layoutTime_gap_bound line 248
  18. lemma OAI.Rokhlin.mixing_nat_of_IsMixing line 267
  19. lemma OAI.Rokhlin.mixingOfOrder_of_sequential line 279
  20. theorem OAI.Rokhlin.mixing_all_finite_orders line 317

    Distinct definitions of this name: ComparatorChallenges/Rokhlin.lean:30 (same statement text; different proof or body). Qualify references as OAI.Rokhlin.mixing_all_finite_orders@path.