OAI/Analysis/IrrationalRotation/Sampling/CirclePhaseSummability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterLaws.block_phase_sum_le line 14
2. theorem OAI.Invariant233.CircleParameterLaws.block_phase_sum_lower line 29
3. theorem OAI.Invariant233.CircleParameterLaws.one_le_block_log_cost line 44
4. theorem OAI.Invariant233.CircleParameterLaws.tsum_block_log_cost_eq_top line 60
5. theorem OAI.Invariant233.CircleParameterLaws.summable_block_phases line 74
6. def OAI.Invariant233.CircleParameterLaws.blocksWithZero line 81
7. theorem OAI.Invariant233.CircleParameterLaws.blocksWithZero_partition line 84
8. theorem OAI.Invariant233.CircleParameterLaws.summable_phases_all line 106
9. theorem OAI.Invariant233.CircleParameterLaws.summable_phases line 119