OAI/Analysis/MatrixSigning/Potential/ShiftFeasibleMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.shift_feasible_of_map_le line 17
2. lemma OAI.CurrentKS.State.endpoint_eta_le line 45
3. lemma OAI.CurrentKS.State.negative_le_operatorNorm line 55
4. lemma OAI.CurrentKS.State.endpoint_value_shift line 62
5. lemma OAI.CurrentKS.State.endpoint_shift_potential line 85
6. lemma OAI.CurrentKS.State.psi_sq_ge_distance line 96
7. lemma OAI.CurrentKS.State.freeze_scalar line 108
8. theorem OAI.CurrentKS.State.freeze_potential line 130