OAI/Geometry/TamingCompatibility/Hodge/HodgeNormalEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HodgeNormalOperator.join_inner line 14
2. lemma OAI.TamingCompatibility.HodgeNormalOperator.output_inner line 17
3. lemma OAI.TamingCompatibility.MetricHodge.full_starTwo_zero line 28
4. lemma OAI.TamingCompatibility.HodgeChart.rawVector_manifoldTest line 42
5. lemma OAI.TamingCompatibility.HodgeChart.manifoldTest_delta_zero_off line 49
6. lemma OAI.TamingCompatibility.HodgeChart.manifoldTest_delta_star_zero_off line 69
7. lemma OAI.TamingCompatibility.HodgeChart.normal_manifoldTest_delta line 90
8. lemma OAI.TamingCompatibility.HodgeChart.normal_energy_point line 105
9. def OAI.TamingCompatibility.HodgeChart.energyPairing line 131
10. lemma OAI.TamingCompatibility.HodgeChart.energyPairing_continuous line 137
11. lemma OAI.TamingCompatibility.HodgeChart.energyPairing_zero_off line 146
12. lemma OAI.TamingCompatibility.HodgeChart.normal_energy_integral line 160