OAI/Analysis/IrrationalRotation/Operators/HilbertEnergyCauchy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.HilbertEnergy.monotone_norm_sq_of_energy line 17
2. theorem OAI.Invariant233.HilbertEnergy.cauchySeq_of_energy line 26
3. theorem OAI.Invariant233.HilbertEnergy.exists_limit_of_energy line 52
4. theorem OAI.Invariant233.HilbertEnergy.limit_norm_sq_eq_iSup line 59
5. theorem OAI.Invariant233.HilbertEnergy.energy_of_inner line 75
6. theorem OAI.Invariant233.HilbertEnergy.cauchySeq_of_inner line 83
7. theorem OAI.Invariant233.HilbertEnergy.exists_limit_of_inner line 90