OAI/Analysis/MatrixSigning/Potential/FacePotential.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.State.norm_coordinate_projection_le_one line 18
  2. lemma OAI.CurrentKS.State.contDiffAt_penalty_coordinate line 25
  3. lemma OAI.CurrentKS.State.penalty_coordinate_jet line 31
  4. lemma OAI.CurrentKS.State.penalty_strip_jet line 38
  5. lemma OAI.CurrentKS.State.penalty_strip_deriv line 47
  6. def OAI.CurrentKS.State.facePotential line 59
  7. def OAI.CurrentKS.State.valueCurve2Bound line 62
  8. def OAI.CurrentKS.State.valueCurve3Bound line 68
  9. def OAI.CurrentKS.State.potentialCurveBound line 75
  10. lemma OAI.CurrentKS.State.valueCurve_bounds_nonneg line 78
  11. lemma OAI.CurrentKS.State.scalar_hundred_bounds line 84
  12. theorem OAI.CurrentKS.State.contDiffAt_facePotential line 96
  13. lemma OAI.CurrentKS.State.line_potential_derivative_bound line 113
  14. theorem OAI.CurrentKS.State.facePotential_strip_derivatives line 122