OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSquareProbabilityBAverageBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.guardIndicator_forall line 16
2. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.average_guardIndicator line 24
3. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualSquareIndicator line 28
4. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualUnitSquareIndicator line 33
5. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualMixedSquareIndicator line 37
6. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.primeResidueIndicatorB_eq_projected_product line 41
7. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualUnitSquareIndicator_average line 50
8. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualMixedSquareIndicator_average line 57