OAI/Analysis/IrrationalRotation/Sampling/SamplingTestTrialBridge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.SamplingTests.average_eq_trialAverage line 12
2. lemma OAI.Invariant233.SamplingTests.spatialLaw_eq_volume line 16
3. lemma OAI.Invariant233.SamplingTests.squaredError_eq_lintegral line 19
4. lemma OAI.Invariant233.SamplingTests.integrable_errorSq_comp line 24
5. lemma OAI.Invariant233.SamplingTests.squaredError_eq_ofReal_integral line 33
6. lemma OAI.Invariant233.SamplingTests.eLpNorm_error_sq_eq_ofReal_integral line 46
7. lemma OAI.Invariant233.SamplingTests.eLpNorm_error_lt_iff_integral_lt line 65
8. theorem OAI.Invariant233.SamplingTests.exists_character_sampling_block_L2 line 80