OAI/NumberTheory/Jacobsthal/Estimates/PairedCostGrouping.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.embedOdd line 15
2. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.embedOdd_measurable line 17
3. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.costKernel_eq_map line 20
4. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.costKernel_odd_lintegral line 28
5. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.costKernel_even_lintegral line 39
6. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.pairedCost_lintegral line 50
7. theorem OAI.Erdos970.NumberTheoryLean.PairedCostGrouping.pairedCost_full_grouping line 64