OAI/Analysis/IrrationalRotation/Rotation/TowerDiagonalApproximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.Rotation.TowerDiagonalApproximation.indicatorClass line 12
  2. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.setProjection_eq_representation line 16
  3. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.coe_sum_ae line 23
  4. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.step_coe_ae line 34
  5. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.sum_setProjection_eq line 54
  6. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.norm_sum_setProjection_sub_representation_le line 63
  7. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.sum_setProjection_mem line 95
  8. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.exists_coefficients_of_small_oscillation line 102
  9. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.exists_mesh_for_norm_approximation line 123
  10. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.tendsto_sum_setProjection_of_error line 139
  11. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.tendsto_sum_setProjection_apply_of_error line 153
  12. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.norm_sum_setProjection_le line 166
  13. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.exists_contractive_V_approximants line 176
  14. theorem OAI.Invariant233.Rotation.TowerDiagonalApproximation.exists_contractive_V_approximants_of_tower_levels line 221