OAI/Geometry/CylinderCovering/Nilpotent/RadialIntegral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderCovering.NilpotentRadialIntegral.radialMap line 10
2. def OAI.CylinderCovering.NilpotentRadialIntegral.parameterRegion line 12
3. lemma OAI.CylinderCovering.NilpotentRadialIntegral.radialMap_hasFDerivAt line 15
4. lemma OAI.CylinderCovering.NilpotentRadialIntegral.radialMap_det line 26
5. lemma OAI.CylinderCovering.NilpotentRadialIntegral.parameterRegion_isClosed line 30
6. lemma OAI.CylinderCovering.NilpotentRadialIntegral.parameterRegion_isCompact line 38
7. lemma OAI.CylinderCovering.NilpotentRadialIntegral.radialMap_injOn line 51
8. theorem OAI.CylinderCovering.NilpotentRadialIntegral.radial_integral line 66