OAI/Geometry/TamingCompatibility/Hodge/HodgeNormalDistribution.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HodgeChart.firstOrder_local line 21
2. lemma OAI.TamingCompatibility.HodgeChart.firstOrder_zero_off line 30
3. lemma OAI.TamingCompatibility.HodgeChart.chart_energy_local line 42
4. def OAI.TamingCompatibility.GeometricHilbert.hodgeDelta line 81
5. abbrev OAI.TamingCompatibility.GeometricHilbert.HodgeDerivativePair line 97
6. abbrev OAI.TamingCompatibility.GeometricHilbert.HodgeGraphSpace line 98
7. def OAI.TamingCompatibility.GeometricHilbert.hodgeGraph line 100
8. def OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy line 108
9. instance OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy_complete line 111
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraph_weak line 114
11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraph_weak_star line 125
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy_weak line 133
13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy_weak_star line 142
14. def OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion line 151
15. def OAI.TamingCompatibility.GeometricHilbert.hodgeWeakDerivative line 154
16. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_injective line 157
17. def OAI.TamingCompatibility.GeometricHilbert.hodgeSmooth line 177
18. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_smooth line 180
19. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_dense line 183