OAI/Probability/RadialTransition/GridPressure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RadialTransition.macroMeasure line 14
2. def OAI.RadialTransition.macroProduct line 17
3. lemma OAI.RadialTransition.macroProduct_nonneg line 21
4. lemma OAI.RadialTransition.integrable_macroProduct line 25
5. lemma OAI.RadialTransition.integral_macroProduct line 33
6. lemma OAI.RadialTransition.macroQuad_upper line 45
7. lemma OAI.RadialTransition.integrable_macroKac line 58
8. lemma OAI.RadialTransition.macroKac_partition_upper line 72