OAI/Analysis/IrrationalRotation/Sampling/TrialSamplingActualMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.TrialSampling.scalar_orientation_mem line 13
2. theorem OAI.Invariant233.TrialSampling.coordinateSample_diagonal_rate line 20
3. theorem OAI.Invariant233.TrialSampling.coordinateSample_cross_error line 28
4. theorem OAI.Invariant233.TrialSampling.coordinateSample_offdiag_error line 39
5. theorem OAI.Invariant233.TrialSampling.scale_le_of_half_horizon line 50
6. theorem OAI.Invariant233.TrialSampling.expectation_squaredError_le_actual_bound line 62
7. theorem OAI.Invariant233.TrialSampling.tendsto_actual_squaredError_zero line 84