OAI/Analysis/BackwardIntertwiners/ErgodicTransitivity.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BackwardIntertwiners.ergodic_late_intersection line 15
  2. lemma OAI.BackwardIntertwiners.measurable_global_coordinate line 60
  3. lemma OAI.BackwardIntertwiners.exists_coordinate_support_nonnull line 64
  4. lemma OAI.BackwardIntertwiners.scalar_invariant_pointwise_orthogonal line 78
  5. lemma OAI.BackwardIntertwiners.fiber_cyclic_orthogonal_order line 99
  6. lemma OAI.BackwardIntertwiners.explicitWeight_quadratic line 133
  7. lemma OAI.BackwardIntertwiners.forwardFiber_weight_coordinates line 136
  8. lemma OAI.BackwardIntertwiners.forwardFiber_lattice line 141
  9. lemma OAI.BackwardIntertwiners.inverseOdometer_ergodic line 155
  10. lemma OAI.BackwardIntertwiners.backwardOperator_power_nonzero line 158
  11. lemma OAI.BackwardIntertwiners.global_invariant_pow line 178
  12. lemma OAI.BackwardIntertwiners.invariant_pointwise_order line 185
  13. lemma OAI.BackwardIntertwiners.forward_backward_scalar_transitive line 203
  14. lemma OAI.BackwardIntertwiners.generated_transitive line 241
  15. def OAI.BackwardIntertwiners.explicitDirectModel line 250
  16. lemma OAI.BackwardIntertwiners.explicitDirectModel_properties line 253
  17. theorem OAI.BackwardIntertwiners.direct_model line 277
  18. def OAI.BackwardIntertwiners.rankOneCoordinate line 280
  19. lemma OAI.BackwardIntertwiners.rankOneCoordinate_apply line 282
  20. lemma OAI.BackwardIntertwiners.rankOneCoordinate_compact line 284
  21. def OAI.BackwardIntertwiners.finiteShift line 288
  22. lemma OAI.BackwardIntertwiners.finiteShift_compact line 290
  23. lemma OAI.BackwardIntertwiners.finiteShift_apply line 293
  24. lemma OAI.BackwardIntertwiners.explicitBeta_outside_bound line 312
  25. lemma OAI.BackwardIntertwiners.finiteShift_error line 324
  26. lemma OAI.BackwardIntertwiners.forwardFiber_compact line 345
  27. abbrev OAI.BackwardIntertwiners.ScalarHilbert line 356
  28. def OAI.BackwardIntertwiners.coordinateL2 line 358
  29. def OAI.BackwardIntertwiners.singleL2 line 361
  30. lemma OAI.BackwardIntertwiners.coordinateL2_ae line 364
  31. lemma OAI.BackwardIntertwiners.singleL2_ae line 367
  32. lemma OAI.BackwardIntertwiners.coordinateL2_singleL2 line 370