OAI/Geometry/TamingCompatibility/Hodge/HodgeLocalCodifferential.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldHodge.pullback_codifferential line 19
2. lemma OAI.TamingCompatibility.ManifoldHodge.pullback_codifferential_star line 37
3. lemma OAI.TamingCompatibility.HodgeChart.cutoffDelta_zero_off line 55
4. lemma OAI.TamingCompatibility.HodgeChart.cutoffDelta_pairing_tsupport line 68
5. lemma OAI.TamingCompatibility.HodgeChart.localDelta_density_integrable line 82
6. lemma OAI.TamingCompatibility.HodgeChart.integral_localDelta_density line 93
7. def OAI.TamingCompatibility.HodgeChart.system line 122
8. lemma OAI.TamingCompatibility.HodgeChart.field_eq line 127
9. lemma OAI.TamingCompatibility.HodgeChart.starredField_local line 133
10. lemma OAI.TamingCompatibility.HodgeChart.system_zero_off line 142
11. lemma OAI.TamingCompatibility.HodgeChart.system_energy line 153
12. lemma OAI.TamingCompatibility.HodgeChart.system_norm_bound line 191
13. lemma OAI.TamingCompatibility.HodgeChart.integral_system_bound line 213