OAI/Probability/ThorpRouting/TraceDecay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.absoluteTrace_even line 13
2. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.Q_square line 23
3. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.levelScale_log line 31
4. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.level_shape_term line 45
5. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.uniform_nonconstant_decay line 73
6. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.tailBound line 129
7. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.two_inverse_twelfth_le line 133
8. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.uniform_tail_bound line 145