OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingTrimming.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.weaklyConverges_iff_tendsto line 16
2. theorem OAI.Invariant233.ProductModel.WeaklyConverges.tendsto_mass line 27
3. theorem OAI.Invariant233.ProductModel.WeaklyConverges.restrict_of_discarded_tendsto_zero line 39
4. theorem OAI.Invariant233.ProductModel.TailTrimming.orderedOrbitSampling_of_untrimmed line 60
5. theorem OAI.Invariant233.ProductModel.TailTrimming.orderedOrbitSampling_of_prefix_samples line 82