Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuFouvryG9GridCarrier

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Grid_label_bounds {N : ℕ} {eps : ℝ} {y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9Carrier N eps) :
(2 ≤ y.2.2 ∧ y.2.2 ≤ N) ∧ (2 ≤ y.2.1 ∧ y.2.1 ≤ N) ∧ 2 ≤ y.1 / y.2.1 ∧ y.1 / y.2.1 ≤ N

All three labels of the actual carrier, including the retained second prime.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Grid_label_bounds · compiled type and proof/definition references.

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridKey (ρ : ℝ) (y : ℕ × ℕ × ℕ) :
ℕ × ℕ × ℕ

The grid uses the ordered labels (n,s,m/s), never the merged pair (n,m).

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridKey · compiled type and proof/definition references.

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed (N : ℕ) (eps ρ : ℝ) :
    Finset (ℕ × ℕ × ℕ)
    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed · compiled type and proof/definition references.

      source
      noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridBox (N : ℕ) (ρ : ℝ) :
      Finset (ℕ × ℕ × ℕ)
      Equations
      Instances For
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridBox · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridKey_bounds {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) {y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9Carrier N eps) :
        (fouvryG9GridKey ρ y).1 ≤ fouvryG9GridIndex ρ ↑N ∧ (fouvryG9GridKey ρ y).2.1 ≤ fouvryG9GridIndex ρ ↑N ∧ (fouvryG9GridKey ρ y).2.2 ≤ fouvryG9GridIndex ρ ↑N
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridKey_bounds · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed_subset {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) :
        fouvryG9GridUsed N eps ρ ⊆ fouvryG9GridBox N ρ
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed_subset · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed_card_le {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) :
        (fouvryG9GridUsed N eps ρ).card ≤ (fouvryG9GridIndex ρ ↑N + 1) ^ 3

        The number of occupied cells is at most the cube of the logarithmic range.

        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridUsed_card_le · compiled type and proof/definition references.