OAI/Geometry/TamingCompatibility/Hodge/HodgeUniformOdd.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_uniform_local_odd line 24
2. lemma OAI.TamingCompatibility.ComplexMatrix.fiberMap_directionalPrincipal line 77
3. lemma OAI.TamingCompatibility.ComplexMatrix.fullShiftedSquare_memSobolev line 82
4. lemma OAI.TamingCompatibility.ComplexMatrix.fullShiftedSquare_commutator_memSobolev line 100
5. def OAI.TamingCompatibility.ComplexMatrix.fullShiftedSquare_commutator_lift line 128
6. lemma OAI.TamingCompatibility.ComplexMatrix.fullShiftedSquare_commutator_lift_spec line 142