OAI/NumberTheory/Ostmann/Arithmetic/MixedCellIntegralFreezingMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogRectangle line 12
2. def OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogDensity line 15
3. def OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogMass line 19
4. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogMass_eq line 22
5. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.residue_mixedLogMass_eq line 38
6. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.isCompact_mixedLogRectangle line 47
7. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.continuousOn_mixedLogDensity line 51
8. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.integrableOn_mixedLogDensity line 59
9. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogDensity_nonneg line 65
10. theorem OAI.Ostmann.Arithmetic.MixedCellIntegralFreezing.mixedLogMass_nonneg line 73