OAI/Probability/FKPressure/Positive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BelowOne.FKPressure.complexSitePolynomial line 14
2. lemma OAI.BelowOne.FKPressure.complexSitePolynomial_real line 21
3. lemma OAI.BelowOne.FKPressure.analyticAt_complexSitePolynomial line 29
4. lemma OAI.BelowOne.FKPressure.complex_pressure_exponential line 45
5. lemma OAI.BelowOne.FKPressure.pressure_coefficient_connected line 78
6. theorem OAI.BelowOne.FKPressure.positive_site_pressure line 100