CubeFreeDensity.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.CubeFreeDensity.bad line 11
Source documentation
Positive integers up to N divisible by a nontrivial integer cube.
```
def bad (N : ℕ) : Finset ℕ := by
…
```
def OAI.Problem337.CubeFreeDensity.good line 16
Source documentation
Positive cube-free integers up to N.
```
def good (N : ℕ) : Finset ℕ := Finset.Icc 1 N \ bad N
```
Mentions: OAI.Problem337.CubeFreeDensity.bad
theorem OAI.Problem337.CubeFreeDensity.mem_bad line 18
theorem OAI.Problem337.CubeFreeDensity.mem_good line 23
theorem OAI.Problem337.CubeFreeDensity.reciprocal_cube_le line 34
Source documentation
A telescoping majorant with no infinite-series or asymptotic input.
```
theorem reciprocal_cube_le (j : ℕ) :
    1 / ((j : ℝ) + 2) ^ 3 ≤
      (1 / 4 : ℝ) * (1 / ((j : ℝ) + 1) - 1 / ((j : ℝ) + 2)) := by
…
```
theorem OAI.Problem337.CubeFreeDensity.sum_reciprocal_cubes_le line 48
Source documentation
The reciprocal cubes starting at two have every finite sum at most one quarter. The intentionally elementary constant leaves room above density 2/3.
```
theorem sum_reciprocal_cubes_le (N : ℕ) :
    (∑ j ∈ Finset.range N, 1 / ((j : ℝ) + 2) ^ 3) ≤ (1 / 4 : ℝ) := by
…
```
theorem OAI.Problem337.CubeFreeDensity.card_positive_multiples line 63
theorem OAI.Problem337.CubeFreeDensity.card_bad_le_sum line 72
Source documentation
An exact finite union bound, including all composite cube bases.
```
theorem card_bad_le_sum (N : ℕ) :
    (bad N).card ≤ ∑ j ∈ Finset.range N, N / (j + 2) ^ 3 := by
…
```
Mentions: OAI.Problem337.CubeFreeDensity.bad
theorem OAI.Problem337.CubeFreeDensity.card_bad_le_quarter line 93
Source documentation
At most one quarter of any initial interval is divisible by a nontrivial cube. This is uniform in the endpoint and has no additive error term.
```
theorem card_bad_le_quarter (N : ℕ) :
    ((bad N).card : ℝ) ≤ (N : ℝ) / 4 := by
…
```
Mentions: OAI.Problem337.CubeFreeDensity.bad
theorem OAI.Problem337.CubeFreeDensity.card_good_ge_three_quarters line 114
Source documentation
Consequently cube-free moduli have the explicit uniform density 3/4.
```
theorem card_good_ge_three_quarters (N : ℕ) :
    (3 : ℝ) * N / 4 ≤ (good N).card := by
…
```
Mentions: OAI.Problem337.CubeFreeDensity.good
theorem OAI.Problem337.CubeFreeDensity.card_good_sdiff_gt_two_thirds line 127
Source documentation
Deleting fewer than N/12 further exceptional moduli still leaves the strict density 2/3 required by the dense rational-supply completion.
```
theorem card_good_sdiff_gt_two_thirds (N : ℕ) (E : Finset ℕ)
    (hE : (E.card : ℝ) < (N : ℝ) / 12) :
    (2 : ℝ) * N / 3 < (good N \ E).card := by
…
```
Mentions: OAI.Problem337.CubeFreeDensity.good
theorem OAI.Problem337.CubeFreeDensity.prime_cube_not_dvd_of_mem_good line 135