OAI/Analysis/IrrationalRotation/Sampling/TrialSamplingMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.TrialSampling.pairLaw_probability line 13
2. lemma OAI.Invariant233.TrialSampling.measurable_coordinateSample line 23
3. theorem OAI.Invariant233.TrialSampling.pairLaw_representative_measurePreserving line 29
4. theorem OAI.Invariant233.TrialSampling.integral_pairLaw_representative line 42
5. theorem OAI.Invariant233.TrialSampling.expectation_squaredError_eq_pair_integral line 52
6. theorem OAI.Invariant233.TrialSampling.memLp_coordinateSample line 77
7. lemma OAI.Invariant233.TrialSampling.measurable_coordinateIdeal line 89
8. theorem OAI.Invariant233.TrialSampling.coordinateIdeal_norm_le line 98
9. theorem OAI.Invariant233.TrialSampling.memLp_coordinateIdeal line 111
10. theorem OAI.Invariant233.TrialSampling.expectation_squaredError_le_meanSquareBound line 118