OAI/Geometry/TamingCompatibility/Hodge/HodgeCommutatorCover.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorPatch line 23
2. def OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorPatch.source line 43
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorPatch.source_open line 46
4. lemma OAI.TamingCompatibility.GeometricHilbert.exists_hodgeCommutatorPatch line 51
5. structure OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover line 61
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCommutatorCover_nonempty line 67
7. def OAI.TamingCompatibility.GeometricHilbert.hodgeCommutatorCover line 81
8. def OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.weight line 104
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.weight_support line 110
10. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.weight_compact line 116
11. def OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.weightedSquare line 121
12. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.weighted_norm_eq line 127
13. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.local_integral_bound line 143
14. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.partition_sum line 166
15. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeCommutatorCover.global_bound line 173
16. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_power_commutator_global_bound line 215