OAI/Geometry/RuledCovering/SingularEnergy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RuledApproximation.singularEnergy line 12
2. lemma OAI.RuledApproximation.singularEnergy_nonneg line 15
3. lemma OAI.RuledApproximation.singularEnergy_measurable line 19
4. lemma OAI.RuledApproximation.singularField_zero line 24
5. lemma OAI.RuledApproximation.singularEnergy_zero line 28
6. lemma OAI.RuledApproximation.singularEnergy_bounded line 31
7. lemma OAI.RuledApproximation.singularEnergy_integrable line 57
8. def OAI.RuledApproximation.energyCorrection line 65
9. lemma OAI.RuledApproximation.energyCorrection_measurable line 69
10. lemma OAI.RuledApproximation.energy_sqrt_ge_one line 74
11. lemma OAI.RuledApproximation.energyCorrection_norm line 80
12. lemma OAI.RuledApproximation.physicalWeight_energy line 90
13. lemma OAI.RuledApproximation.physicalWeight_energy_expansion line 98
14. lemma OAI.RuledApproximation.energyCorrection_tendsto line 110
15. lemma OAI.RuledApproximation.singularDomain_subset_cone line 122
16. lemma OAI.RuledApproximation.singularDomain_eventually_mem line 126
17. lemma OAI.RuledApproximation.energyCorrection_integral_tendsto line 147