OAI/Algebra/AlgebraicObstruction/CorrectionOperator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.sum line 14
2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.positively_weighted_triple line 21
3. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.correctionArguments line 35
4. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.remainderValue line 40
5. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.correctionOperator line 45
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.correctionArguments_centered line 51
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.correctionArguments_jet line 63
8. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.remainderValue_positive line 81
9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.remainderValue_jet line 91
10. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.correctionOperator_contracts line 100
11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.exists_correction_matrix line 121