OAI/Probability/FKPressure/Taylor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BelowOne.FKPressure.reachable_image_of_adj_reachable line 14
2. lemma OAI.BelowOne.FKPressure.connected_types_of_component_count line 24
3. lemma OAI.BelowOne.FKPressure.connectedSum_eq_zero_of_disconnected_types line 75
4. lemma OAI.BelowOne.FKPressure.pressure_derivative_eq_zero_of_disconnected_types line 95
5. lemma OAI.BelowOne.FKPressure.taylor_coordinate_connected line 117