OAI/Analysis/ModularRecovery/ErgodicAverages.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space and predual ergodic averaging for the modular action.

  1. lemma OAI.BoundedRecovery.StandardModularData.sigma_mem line 19
  2. lemma OAI.BoundedRecovery.StandardModularData.sigma_apply_xi line 22
  3. lemma OAI.BoundedRecovery.StandardModularData.sigma_one line 26
  4. lemma OAI.BoundedRecovery.StandardModularData.sigma_mul line 29
  5. lemma OAI.BoundedRecovery.StandardModularData.sigma_star line 37
  6. lemma OAI.BoundedRecovery.StandardModularData.sigma_add line 41
  7. lemma OAI.BoundedRecovery.StandardModularData.sigma_smul line 44
  8. lemma OAI.BoundedRecovery.StandardModularData.norm_sigma line 47
  9. lemma OAI.BoundedRecovery.StandardModularData.state_sigma line 57
  10. lemma OAI.BoundedRecovery.StandardModularData.continuous_sigma_apply line 64
  11. lemma OAI.BoundedRecovery.StandardModularData.fixed_of_fixed_vector line 69
  12. lemma OAI.BoundedRecovery.StandardModularData.norm_star_apply_xi_le line 77
  13. lemma OAI.BoundedRecovery.StandardModularData.state_star_mul line 89
  14. lemma OAI.BoundedRecovery.convex_bounded_orbit line 107
  15. lemma OAI.BoundedRecovery.small_on_separating_controls_vector line 120
  16. lemma OAI.BoundedRecovery.convex_minimizer_unique line 166
  17. lemma OAI.BoundedRecovery.exists_fixed_in_closed_convex_orbit line 178
  18. lemma OAI.BoundedRecovery.map_mem_closed_convexHull line 199
  19. lemma OAI.BoundedRecovery.StandardModularData.inner_fixed_on_closed_convex_orbit line 219
  20. lemma OAI.BoundedRecovery.StandardModularData.fixed_eq_state_of_mem_closed_convex_orbit line 231
  21. lemma OAI.BoundedRecovery.StandardModularData.state_mem_closed_convex_orbit line 248
  22. lemma OAI.BoundedRecovery.StandardModularData.pair_state_mem_closed_convex_orbit line 259
  23. lemma OAI.BoundedRecovery.StandardModularData.exists_finite_average_pair line 300
  24. lemma OAI.BoundedRecovery.re_vectorState_star_mul_nonneg line 344
  25. lemma OAI.BoundedRecovery.re_vectorState_sq line 349
  26. def OAI.BoundedRecovery.StandardModularData.sigmaLinear line 364
  27. lemma OAI.BoundedRecovery.StandardModularData.sigmaLinear_apply line 369
  28. lemma OAI.BoundedRecovery.StandardModularData.sigma_sum line 372
  29. lemma OAI.BoundedRecovery.StandardModularData.sigma_real_smul line 376
  30. lemma OAI.BoundedRecovery.StandardModularData.state_eq_vectorState line 379
  31. lemma OAI.BoundedRecovery.StandardModularData.state_sum line 382
  32. lemma OAI.BoundedRecovery.StandardModularData.state_real_smul line 386
  33. lemma OAI.BoundedRecovery.StandardModularData.state_sandwich line 389
  34. lemma OAI.BoundedRecovery.StandardModularData.state_covariant_sandwich line 394
  35. lemma OAI.BoundedRecovery.StandardModularData.norm_state_le line 400
  36. lemma OAI.BoundedRecovery.StandardModularData.norm_state_real_star_mul line 406
  37. lemma OAI.BoundedRecovery.StandardModularData.state_star_mul_re line 412
  38. lemma OAI.BoundedRecovery.StandardModularData.state_mul_star line 415
  39. lemma OAI.BoundedRecovery.StandardModularData.state_sq_re line 419