OAI/Geometry/TranslativeCovering/PeriodicDensity.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.TranslativeCovering.PeriodicCoverline 114 - def
OAI.TranslativeCovering.PeriodicCover.intensityline 122 - def
OAI.TranslativeCovering.thetaPerListedline 125 - lemma
OAI.TranslativeCovering.PeriodicCover.cubic_leline 128 - def
OAI.TranslativeCovering.CubicCover.toPeriodicline 142 - lemma
OAI.TranslativeCovering.CubicCover.toPeriodic_intensityline 154 - theorem
OAI.TranslativeCovering.periodization_allline 162