OAI/NumberTheory/Ostmann/Construction/FiniteTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.FinitePrior.cmean line 12
2. theorem OAI.Ostmann.Construction.FinitePrior.norm_cmean_le line 14
3. theorem OAI.Ostmann.Construction.FinitePrior.norm_cmean_sq_le line 22
4. theorem OAI.Ostmann.Construction.FinitePrior.mean_mono line 29
5. theorem OAI.Ostmann.Construction.row_cauchy line 35
6. theorem OAI.Ostmann.Construction.extracted_row_transfer line 42
7. theorem OAI.Ostmann.Construction.extend_nonnegative_pivot_sum line 51