OAI/Analysis/IrrationalRotation/Product/ProductBlockCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.one_le_block_cost line 11
2. theorem OAI.Invariant233.ProductModel.tsum_block_coordinate_cost_eq_top line 34
3. theorem OAI.Invariant233.ProductModel.hasNegInfiniteLogIntegral_of_block_bounds line 55
4. theorem OAI.Invariant233.ProductModel.exists_admissible_block_weight line 66