OAI/Probability/FKPressure/ComplexSeries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BelowOne.PressureSeries.complexify line 14
2. lemma OAI.BelowOne.PressureSeries.complexify_apply line 20
3. lemma OAI.BelowOne.PressureSeries.complexify_real line 27
4. lemma OAI.BelowOne.PressureSeries.complexify_norm_le line 36
5. lemma OAI.BelowOne.PressureSeries.complexify_radius line 58
6. lemma OAI.BelowOne.PressureSeries.norm_lt_of_coordinates line 71
7. lemma OAI.BelowOne.PressureSeries.complexify_hasSum line 75
8. lemma OAI.BelowOne.PressureSeries.complexify_sum_real line 88