OAI/Probability/SignedSweeps/MomentMonotonicity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.power_on_eigenvector line 10
2. lemma OAI.SignedSweeps.trace_power_spectral line 18
3. lemma OAI.SignedSweeps.positive_contraction_eigenvalue_bounds line 31
4. lemma OAI.SignedSweeps.trace_power_antitone line 43
5. lemma OAI.SignedSweeps.weightedMoment_antitone line 55
6. lemma OAI.SignedSweeps.moment_bound_of_le_one line 62
7. lemma OAI.SignedSweeps.finite_depth_signed_moment_bound line 74