OAI/Analysis/IrrationalRotation/Sampling/TrialSamplingSelection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.TrialSampling.spatialLaw_probability line 14
2. lemma OAI.Invariant233.TrialSampling.phaseLaw_probability line 20
3. lemma OAI.Invariant233.TrialSampling.phaseLaw_eq_pi line 29
4. lemma OAI.Invariant233.TrialSampling.measurable_kernel_pair line 38
5. lemma OAI.Invariant233.TrialSampling.measurable_orientedKernel_pair line 50
6. lemma OAI.Invariant233.TrialSampling.measurable_average_pair line 58
7. lemma OAI.Invariant233.TrialSampling.measurable_squaredError line 77
8. lemma OAI.Invariant233.TrialSampling.squaredError_eq_eLpNorm_sq line 81
9. lemma OAI.Invariant233.TrialSampling.squaredError_lt_iff_eLpNorm_lt line 96
10. theorem OAI.Invariant233.TrialSampling.exists_strict_trials_of_moment_budget line 106
11. lemma OAI.Invariant233.TrialSampling.tendsto_failureBound_nat line 154
12. theorem OAI.Invariant233.TrialSampling.eventually_exists_strict_trials_of_moments_tendsto_zero line 160
13. theorem OAI.Invariant233.TrialSampling.exists_strict_trials_with_source_L2_bound line 201