OAI/Probability/FKPressure/Coefficients.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BelowOne.PressureSeries.Labels line 13
2. def OAI.BelowOne.PressureSeries.multiplicity line 15
3. lemma OAI.BelowOne.PressureSeries.sum_multiplicity line 18
4. lemma OAI.BelowOne.PressureSeries.multiplicity_pos line 23
5. lemma OAI.BelowOne.PressureSeries.prod_multiplicity line 26
6. def OAI.BelowOne.PressureSeries.weight line 36
7. def OAI.BelowOne.PressureSeries.coefficient line 39
8. lemma OAI.BelowOne.PressureSeries.coefficient_nonneg line 43
9. lemma OAI.BelowOne.PressureSeries.coefficient_zero line 47
10. lemma OAI.BelowOne.PressureSeries.coefficient_pos_has_label line 60
11. lemma OAI.BelowOne.PressureSeries.summable_labels line 69
12. lemma OAI.BelowOne.PressureSeries.summable_complex_labels line 89
13. lemma OAI.BelowOne.PressureSeries.fiber_complex line 101
14. lemma OAI.BelowOne.PressureSeries.hasSum_coefficients_of_complex_degrees line 110