OAI/Probability/ThorpResults/UniformMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.weightedMoment line 13

   Distinct definitions of this name: ComparatorChallenges/ThorpRemaining.lean:445 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.LowPlanes.weightedMoment@path.

2. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.trace_mul_power_comm line 18
3. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.uniform_weighted_moment line 30
4. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.four_row_fixed_moment line 81
5. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.bounded_regular_schatten_moment line 94
6. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.dyadic_negative_power_le line 113
7. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.bounded_regular_moment line 120