OAI/Analysis/StrictMeans/Eigenmeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.scaled_power line 45
2. def OAI.StrictInverseFirstPower.growthResolvent line 48
3. lemma OAI.StrictInverseFirstPower.summable_growthResolvent line 50
4. lemma OAI.StrictInverseFirstPower.growthResolvent_mul line 55
5. lemma OAI.StrictInverseFirstPower.mul_growthResolvent line 68
6. lemma OAI.StrictInverseFirstPower.growthResolvent_apply_series line 84
7. lemma OAI.StrictInverseFirstPower.growthResolvent_monotone line 97
8. lemma OAI.StrictInverseFirstPower.growthResolvent_unit_ge_one line 114
9. lemma OAI.StrictInverseFirstPower.exists_approximate_eigenprobability line 142
10. theorem OAI.StrictInverseFirstPower.exists_exact_eigenprobability line 223