OAI/Probability/SKGap/Localization/LocalStartedDiagonal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.implicit_started_diagonal_local line 20
2. def OAI.SKGap.Noncrossing.ClosedMarked.pairBudget line 100
3. lemma OAI.SKGap.Noncrossing.ClosedMarked.pairBudget_nonneg line 101
4. lemma OAI.SKGap.Noncrossing.ClosedMarked.mass_nonneg line 102
5. lemma OAI.SKGap.Noncrossing.ClosedMarked.smallBranch_budget line 105
6. lemma OAI.SKGap.Noncrossing.ClosedMarked.boundedBranch_budget line 110
7. lemma OAI.SKGap.Noncrossing.ClosedMarked.implicitPair_pairBudget line 117
8. lemma OAI.SKGap.Noncrossing.ClosedMarked.implicitPair_budget_le line 124
9. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.smallBranches_budget line 143
10. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.boundedBranches_budget line 153