OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairSquareProbabilityProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.probability_nonneg line 13
2. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.product_relative_loss line 16
3. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.occurrence_reciprocal_eq_fibers line 47
4. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualUnitSquareProbability line 59
5. def OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actualMixedSquareProbability line 64
6. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actual_unit_square_product_loss line 69
7. theorem OAI.Ostmann.Arithmetic.HistoryPairSquareProbability.actual_mixed_square_product_loss line 90