OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairVariableBAverageDefs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualLeftAt line 17
2. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualRightAt line 21
3. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualLeftAt_cast line 25
4. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualRightAt_cast line 32
5. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualUnitSquareProbabilityAt line 39
6. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualMixedSquareProbabilityAt line 44
7. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualSquareIndicatorAt line 49
8. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualUnitSquareIndicatorAt line 55
9. def OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualMixedSquareIndicatorAt line 59
10. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualUnitSquareIndicatorAt_average line 63
11. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.actualMixedSquareIndicatorAt_average line 70
12. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.unit_baseAt_eq_actualProbability line 77
13. lemma OAI.Ostmann.Arithmetic.HistoryPairVariableBAverage.mixed_baseAt_eq_actualProbability line 86