OAI/Probability/SignedSweeps/SpectralGap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.sweepOperator_norm_lt_one line 11
2. lemma OAI.SignedSweeps.linear_pow_bound line 20
3. lemma OAI.SignedSweeps.linear_trace_bound line 29
4. lemma OAI.SignedSweeps.positiveSquare_norm line 45
5. lemma OAI.SignedSweeps.weightedMoment_le_opNorm line 53
6. lemma OAI.SignedSweeps.weightedMoment_tendsto_zero line 69
7. lemma OAI.SignedSweeps.eventually_weightedMoment_le_one line 79