OAI/Probability/RadialTransition/BoxPressure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.summable_sectorWeight line 14
2. lemma OAI.RadialTransition.sectorWeight_tsum line 18
3. lemma OAI.RadialTransition.macroProduct_sector line 23
4. lemma OAI.RadialTransition.macroSector_lower line 35
5. lemma OAI.RadialTransition.macroKac_partition_lower line 50