OAI/Analysis/MatrixSigning/Potential/NormCoordinate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.State.norm_coordinate_le line 26
2. lemma OAI.CurrentKS.State.jetBound_S line 33
3. lemma OAI.CurrentKS.State.jetBound_psi_coordinate line 51
4. lemma OAI.CurrentKS.State.norm_sandwich_coefficient line 59
5. lemma OAI.CurrentKS.State.contDiffAt_psi_coordinate line 66
6. lemma OAI.CurrentKS.State.jetBound_eta_term line 73
7. lemma OAI.CurrentKS.State.jetBound_eta line 81