OAI/Analysis/IrrationalRotation/Rotation/CircleMarginalBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.CircleParameterLaws.budgetBlocks line 16
2. theorem OAI.Invariant233.CircleParameterLaws.budgetBlocks_partition line 19
3. theorem OAI.Invariant233.CircleParameterLaws.normalized_block_budget line 41
4. theorem OAI.Invariant233.CircleParameterData.summable_kappa_sq line 116

   Distinct definitions of this name: OAI/Analysis/IrrationalRotation/Analysis/BlockMassRegrouping.lean:114 (different declaration text). Qualify references as OAI.Invariant233.CircleParameterData.summable_kappa_sq@path.

5. theorem OAI.Invariant233.CircleParameterLaws.circle_marginal_budget line 131