OAI/Analysis/Mahler/SourceCanonicalMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.measurePreserving_coordinateCast line 9
2. lemma OAI.Mahler.measurePreserving_sourceCoordinates line 14
3. theorem OAI.Mahler.setIntegral_sourceCoordinates line 19
4. lemma OAI.Mahler.radiusSq_coordinateCast line 25
5. lemma OAI.Mahler.norm_sourceCoordinates_sq line 30