OAI/Analysis/IrrationalRotation/Rotation/CountableWeightRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantProjection.CountableWeightRange.exp_tsum_mem_finite_cost_values line 13
2. theorem OAI.InvariantProjection.CountableWeightRange.countable_exp_tsum_image line 32
3. theorem OAI.InvariantProjection.CountableWeightRange.ae_exp_tsum_mem_countable line 41
4. theorem OAI.InvariantProjection.CountableWeightRange.finite_cost_values_subset_Ioc line 51
5. theorem OAI.InvariantProjection.CountableWeightRange.floor_add_zero_or_one line 59
6. theorem OAI.InvariantProjection.CountableWeightRange.ae_floor_weight_mem_countable line 66