OAI/Analysis/IrrationalRotation/Spectral/PositivePartialResolvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.PositivePartialResolvent.graphSum line 15
2. theorem OAI.Invariant233.PositivePartialResolvent.graphSum_apply line 19
3. theorem OAI.Invariant233.PositivePartialResolvent.norm_le_norm_add line 22
4. theorem OAI.Invariant233.PositivePartialResolvent.graphSum_bound line 33
5. theorem OAI.Invariant233.PositivePartialResolvent.graphSum_range_orthogonal line 43
6. theorem OAI.Invariant233.PositivePartialResolvent.exists_add_apply_eq line 73
7. theorem OAI.Invariant233.PositivePartialResolvent.exists_resolvent line 90