OAI/Analysis/IrrationalRotation/Spectral/PositivePartialResolventAlternative.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.PositivePartialResolventAlternative.graphSum line 16
  2. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphSum_apply line 21
  3. theorem OAI.Invariant233.PositivePartialResolventAlternative.norm_coordinates_le line 26
  4. theorem OAI.Invariant233.PositivePartialResolventAlternative.norm_le_graphSum line 39
  5. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphSum_injective_closedRange line 47
  6. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphSum_orthogonal_eq_bot line 56
  7. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphSum_bijective line 88
  8. def OAI.Invariant233.PositivePartialResolventAlternative.graphInverse line 97
  9. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphSum_graphInverse line 102
  10. theorem OAI.Invariant233.PositivePartialResolventAlternative.graphInverse_graphSum line 108
  11. def OAI.Invariant233.PositivePartialResolventAlternative.resolvent line 114
  12. theorem OAI.Invariant233.PositivePartialResolventAlternative.resolvent_apply line 123
  13. theorem OAI.Invariant233.PositivePartialResolventAlternative.resolvent_mem_domain line 127
  14. theorem OAI.Invariant233.PositivePartialResolventAlternative.add_apply_resolvent line 132
  15. theorem OAI.Invariant233.PositivePartialResolventAlternative.apply_resolvent line 144
  16. theorem OAI.Invariant233.PositivePartialResolventAlternative.resolvent_add_apply line 150
  17. theorem OAI.Invariant233.PositivePartialResolventAlternative.norm_resolvent_le line 156
  18. theorem OAI.Invariant233.PositivePartialResolventAlternative.range_resolvent line 166
  19. theorem OAI.Invariant233.PositivePartialResolventAlternative.resolvent_injective line 175
  20. theorem OAI.Invariant233.PositivePartialResolventAlternative.resolvent_denseRange line 188