OAI/Geometry/TamingCompatibility/Hodge/HodgeCubeBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.norm_cube_combination_le line 12
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_cube_commutator_global_bound line 41
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCubeCommutator_apply line 70
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCubeCommutator_pairing line 74
5. lemma OAI.TamingCompatibility.norm_le_of_dense_pair_bound line 92
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_relative_antiprojection line 116