OAI/Geometry/CylinderCovering/Nilpotent/IntegralSpecialization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.Nilpotent.truncatedLabels_eq_radial_image line 13
2. lemma OAI.CylinderCovering.Nilpotent.angularWeight_continuous line 24
3. lemma OAI.CylinderCovering.Nilpotent.physicalWeight_angularField line 32
4. lemma OAI.CylinderCovering.Nilpotent.half_le_height line 41
5. theorem OAI.CylinderCovering.Nilpotent.truncatedLabels_weight_integral line 47
6. theorem OAI.CylinderCovering.Nilpotent.truncatedLabels_weight_integral_le line 62