OAI/Geometry/TamingCompatibility/Hodge/HodgeWedgeEnergy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.MetricHodge.full_wedge_energy line 17
2. lemma OAI.TamingCompatibility.hodgeStar_add line 58
3. lemma OAI.TamingCompatibility.hodgeStar_smul line 68
4. lemma OAI.TamingCompatibility.hodgeStar_pairing line 78
5. def OAI.TamingCompatibility.GeometricHilbert.preStar line 91
6. lemma OAI.TamingCompatibility.GeometricHilbert.preStar_square line 103
7. def OAI.TamingCompatibility.GeometricHilbert.l2Star line 107
8. lemma OAI.TamingCompatibility.GeometricHilbert.l2Star_smooth line 112
9. lemma OAI.TamingCompatibility.GeometricHilbert.l2Star_square line 118
10. lemma OAI.TamingCompatibility.GeometricHilbert.l2Star_norm line 125
11. lemma OAI.TamingCompatibility.GeometricHilbert.l2Star_inner line 132
12. lemma OAI.TamingCompatibility.GeometricHilbert.l2Star_self_adjoint line 138
13. lemma OAI.TamingCompatibility.hodgeStar_fun_smul line 161
14. lemma OAI.TamingCompatibility.codifferential_fun_smul line 167
15. lemma OAI.TamingCompatibility.full_pairing_star_wedge line 187
16. lemma OAI.TamingCompatibility.full_cutoff_delta_pointwise line 205