OAI/NumberTheory/Jacobsthal/Partitions/CommonCellSum.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.ContinuousParentBins.multiplier_source_ratio line 18
2. theorem OAI.Erdos970.NumberTheoryLean.ContinuousParentBins.continuous_bin_mass_ratio line 25
3. theorem OAI.Erdos970.NumberTheoryLean.ContinuousParentBins.continuousBin_parent_ratio line 35
4. theorem OAI.Erdos970.NumberTheoryLean.ContinuousParentBins.positive_ratio_error line 42
5. theorem OAI.Erdos970.NumberTheoryLean.ContinuousParentBins.continuous_parent_bin_error line 54
6. theorem OAI.Erdos970.NumberTheoryLean.NearbyParentFullBins.nearby_parent_full_bin_error line 87
7. def OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.upperSupport line 139
8. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.prime_child_interval line 141
9. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.prime_row_interval line 158
10. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.costKernel_lower_support line 171
11. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.continuous_interval_measurable line 180
12. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.continuous_low_interval line 185
13. theorem OAI.Erdos970.NumberTheoryLean.ActualSupportIntervals.continuous_row_interval line 206
14. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.prime_label_eq_bin line 228
15. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.continuous_label_mass_eq_bin line 241
16. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.cell_below_S_not_cemetery line 257
17. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.mesh_cells_disjoint line 267
18. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.continuous_mesh_sum_le_one line 281
19. theorem OAI.Erdos970.NumberTheoryLean.ActualMeshBins.common_cell_error line 295
20. theorem OAI.Erdos970.NumberTheoryLean.CommonCellSum.common_cell_sum_error line 339