OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairReferenceFlagExpectationSelectedFamily.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily line 18
2. def OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily.mean line 43
3. def OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily.WeightBound line 48
4. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily.sameLeft line 51
5. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily.sameRight line 58
6. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagExpectation.ActiveBlockFamily.zero_or_reference line 65