OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSquareProbabilityAverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean line 10
2. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.probability_eq_rmean line 13
3. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_nonneg line 17
4. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_mono line 21
5. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_sub line 25
6. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_mul_left line 29
7. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_equiv line 34
8. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.rmean_prod line 39
9. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.base_average_lift_loss line 45