OAI/Analysis/IrrationalRotation/Main.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Irrational rotation counterexamples, product realizations, and transitive commutants.

  1. theorem OAI.Invariant233.Results.rotation_hyperfinite line 52
  2. theorem OAI.Invariant233.Results.circle_parameters_exist line 57
  3. theorem OAI.Invariant233.Results.commutant_properness line 65
  4. theorem OAI.Invariant233.Results.commutant_affine_shift line 70
  5. theorem OAI.Invariant233.Results.commutant_algebra line 75
  6. theorem OAI.Invariant233.Results.hyperinvariant_projection_mem line 83
  7. theorem OAI.Invariant233.Results.finite_convolution_uniform_lower_bound line 93
  8. theorem OAI.Invariant233.Results.uniform_irrational_rotation_average line 102
  9. theorem OAI.Invariant233.product_density_bound line 113
  10. theorem OAI.Invariant233.conditional_convolution line 135
  11. theorem OAI.Invariant233.scalar_multiplier_fields line 148
  12. theorem OAI.Invariant233.rational_graphs line 171
  13. theorem OAI.Invariant233.Results.continuous_counterexample_quasinilpotent line 188
  14. theorem OAI.Invariant233.Results.product_triangular_law_properties line 194
  15. theorem OAI.Invariant233.product_quasinilpotent line 203
  16. theorem OAI.Invariant233.product_phase_ranges line 233
  17. theorem OAI.Invariant233.compact_transfer line 261
  18. theorem OAI.Invariant233.scalar_sampling_estimates line 289
  19. theorem OAI.Invariant233.positive_diagonal line 299
  20. theorem OAI.Invariant233.product_ordinary_tail_projection line 329
  21. theorem OAI.Invariant233.product_polar_structure line 349
  22. theorem OAI.Invariant233.Results.rotation_factor_structure line 359
  23. theorem OAI.Invariant233.conditional_labels line 368
  24. theorem OAI.Invariant233.product_coupling_marginals line 373
  25. theorem OAI.Invariant233.truncation_bound line 387
  26. theorem OAI.Invariant233.digit_marginals line 405
  27. theorem OAI.Invariant233.ordered_couplings line 414
  28. theorem OAI.Invariant233.tail_attenuation line 432
  29. theorem OAI.Invariant233.product_factor line 442
  30. theorem OAI.Invariant233.affiliated_transport line 459
  31. theorem OAI.Invariant233.Results.transitive_commutant_on_separable_hilbert line 488
  32. theorem OAI.Invariant233.Results.cho_ko_lee_comparison line 505
  33. theorem OAI.Invariant233.product_pair_identity line 521
  34. theorem OAI.Invariant233.product_biased_identity line 539
  35. theorem OAI.Invariant233.measurable_counterexample line 564
  36. theorem OAI.Invariant233.product_finite_coordinate_sampling line 585
  37. abbrev OAI.Invariant233.ProductModel.CounterexampleFiber line 603

    Also declared: ComparatorChallenges/IrrationalRotation.lean:769 (same declaration text).

  38. abbrev OAI.Invariant233.ProductModel.CounterexampleHilbert line 606

    Also declared: ComparatorChallenges/IrrationalRotation.lean:772 (same declaration text).

  39. instance OAI.Invariant233.ProductModel.instCompleteSpaceHilbertCounterexample line 612

    Also declared: ComparatorChallenges/IrrationalRotation.lean:778 (same declaration text).

  40. def OAI.Invariant233.ProductOperatorProperties line 615

    Also declared: ComparatorChallenges/IrrationalRotation.lean:781 (same declaration text).

  41. def OAI.Invariant233.ProductModel.counterexampleHilbertNormedAddCommGroup line 629

    Also declared: ComparatorChallenges/IrrationalRotation.lean:795 (same declaration text).

  42. def OAI.Invariant233.ProductModel.counterexampleHilbertInnerProductSpace line 638

    Also declared: ComparatorChallenges/IrrationalRotation.lean:804 (same declaration text).

  43. def OAI.Invariant233.ProductModel.HasCounterexampleOperator line 649

    Also declared: ComparatorChallenges/IrrationalRotation.lean:815 (same declaration text).

  44. def OAI.Invariant233.ProductModel.IsCounterexampleRealization line 656

    Also declared: ComparatorChallenges/IrrationalRotation.lean:822 (same declaration text).

  45. theorem OAI.Invariant233.Results.product_realization line 670

    Distinct definitions of this name: ComparatorChallenges/IrrationalRotation.lean:843 (same statement text; different proof or body). Qualify references as OAI.Invariant233.Results.product_realization@path.