OAI/Probability/RadialTransition/IdealAttainment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.entropy_lower line 10
2. lemma OAI.RadialTransition.grandPressure_continuous_h line 19
3. lemma OAI.RadialTransition.branch_le_density_value line 30
4. lemma OAI.RadialTransition.branch_le_density_branch line 37
5. lemma OAI.RadialTransition.density_value_neg line 45
6. lemma OAI.RadialTransition.ideal_density_cofinal line 55
7. lemma OAI.RadialTransition.ideal_exists_active_of_density_bound line 73
8. lemma OAI.RadialTransition.active_density_bound line 90