OAI/Geometry/TamingCompatibility/Hodge/HodgeWeightNorm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateFunction line 28
2. def OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateSupport line 31
3. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateSupport_compact line 35
4. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateSupport_subset line 41
5. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateSupport_target line 47
6. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateFunction_smooth_compact line 53
7. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.coordinateFunction_support line 65
8. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.density_sqrt_smooth line 77
9. def OAI.TamingCompatibility.GeometricHilbert.LocalWeight.halfDensity line 81
10. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.halfDensity_apply line 88
11. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.halfDensity_support line 92
12. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.halfDensity_compact line 96
13. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.integral_weight_norm line 99
14. lemma OAI.TamingCompatibility.GeometricHilbert.LocalWeight.integral_weight_H0_norm line 128