OAI/Analysis/IrrationalRotation/Operators/ColumnOperator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Fields.denseRange_basis_linearCombination line 14
  2. theorem OAI.Invariant233.Fields.columnOperator_linearCombination line 20
  3. theorem OAI.Invariant233.Fields.columnOperator_apply_basis line 29
  4. theorem OAI.Invariant233.Fields.norm_columnOperator_le line 37
  5. theorem OAI.Invariant233.Fields.columnOperator_unique line 44
  6. theorem OAI.Invariant233.Fields.denseRange_rationalComplex line 53
  7. theorem OAI.Invariant233.Fields.finite_combination_bound_of_rational line 64
  8. theorem OAI.Invariant233.Fields.stronglyMeasurable_columnOperator_apply line 88
  9. theorem OAI.Invariant233.Fields.aestronglyMeasurable_columnOperator_apply line 100
  10. theorem OAI.Invariant233.Fields.ae_finite_combination_bound_of_rational line 116
  11. theorem OAI.Invariant233.Fields.exists_bounded_field_of_rational_column_tests line 131