OAI/Analysis/IrrationalRotation/Couplings/BlockProductCoupling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.OrderedProductCoupling.sourceKappa_nonneg line 15
2. lemma OAI.Invariant233.OrderedProductCoupling.sourceKappa_pos line 19
3. lemma OAI.Invariant233.OrderedProductCoupling.sourceKappa_le line 23
4. lemma OAI.Invariant233.OrderedProductCoupling.summable_sourceKappa_sq line 28
5. lemma OAI.Invariant233.OrderedProductCoupling.blockDensityBound_pos line 38
6. lemma OAI.Invariant233.OrderedProductCoupling.blockDensityBound_sq line 41
7. lemma OAI.Invariant233.OrderedProductCoupling.energyBound_ofBlocks line 55
8. theorem OAI.Invariant233.OrderedProductCoupling.ofBlocks_energy_sum line 62
9. theorem OAI.Invariant233.OrderedProductCoupling.exists_hybrid_density_ofBlocks line 85
10. theorem OAI.Invariant233.OrderedProductCoupling.exists_source_hybrid_density line 103
11. theorem OAI.Invariant233.OrderedProductCoupling.exists_source_consecutive_couplings line 117