OAI/Analysis/MatrixSigning/Potential/Norm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Movement.norm_one_le line 18
2. lemma OAI.CurrentKS.Movement.inverse_geometric_bound line 23
3. lemma OAI.CurrentKS.Movement.inverse_woodbury_sqrt line 33
4. lemma OAI.CurrentKS.Movement.inverse_product_bound line 53
5. lemma OAI.CurrentKS.Movement.response_norm_bound line 82
6. lemma OAI.CurrentKS.Movement.coupled_response_energy_bound line 110