OAI/Probability/ThorpResults/FullDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2Squared line 14

   Also declared: ComparatorChallenges/ThorpRemaining.lean:469 (same declaration text).

2. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2SquaredFrom line 18

   Also declared: ComparatorChallenges/ThorpRemaining.lean:473 (same declaration text).

3. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2SquaredFrom_eq line 22
4. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2Squared_nonneg line 29
5. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.density_fourier_bound line 33
6. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.density_forward_bound line 63
7. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.fixed_sweep_density_decay line 78
8. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.fixed_sweep_density_convergence line 88
9. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.fixed_sweep_mixing line 102