OAI/Algebra/AlgebraicObstruction/PotentialReplacement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wallCoordinates line 15
2. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wallCoordinates_centered line 18
3. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wallEval line 24
4. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.subst_potential_eq_sum line 30
5. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wallEval_negativeSlope line 41
6. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.origin_le_jacobson line 70
7. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wall_error_bounds line 78
8. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.wall_ambient_derivative_mem line 100
9. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.potential_sub line 125
10. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.gradient_sub line 135
11. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.gradient_mem_of_wall_derivatives line 145
12. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticData.replace line 163