Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11CofactorWindow

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_rough_iff_survives (q : ℝ) (m : ℕ) :
LiLiuPrereqBuchstab.Rough q m ↔ SurvivesSieve 1 q m
Inspect dependencies

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

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) :
Finset ℕ

The actual positive-natural carrier, with a strict lower and closed upper endpoint.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11CofactorWindow_iff {N m : ℕ} {ε : ℝ} {v : GoldbachG11Label} :
    m ∈ goldbachG11CofactorWindow N ε v ↔ 0 < m ∧ ε * (↑N / ↑(goldbachG11LabelProd v)) < ↑m ∧ ↑m ≤ ↑N / ↑(goldbachG11LabelProd v) ∧ SurvivesSieve 1 (↑v.snd.snd.snd) m
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.one_mem_goldbachG11CofactorWindow {N : ℕ} {ε : ℝ} {v : GoldbachG11Label} :
    1 ∈ goldbachG11CofactorWindow N ε v ↔ ε * (↑N / ↑(goldbachG11LabelProd v)) < 1 ∧ 1 ≤ ↑N / ↑(goldbachG11LabelProd v)
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_prefix_subset (N : ℕ) {ε : ℝ} (hε : ε ∈ Set.Icc 0 1) (v : GoldbachG11Label) :
    LiLiuPrereqBuchstab.roughNumbers (ε * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd ⊆ LiLiuPrereqBuchstab.roughNumbers (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_card (N : ℕ) {ε : ℝ} (hε : ε ∈ Set.Icc 0 1) (v : GoldbachG11Label) :
    (goldbachG11CofactorWindow N ε v).card = LiLiuPrereqBuchstab.roughCount (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd - LiLiuPrereqBuchstab.roughCount (ε * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_card_real (N : ℕ) {ε : ℝ} (hε : ε ∈ Set.Icc 0 1) (v : GoldbachG11Label) :
    ↑(goldbachG11CofactorWindow N ε v).card = ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd) - ↑(LiLiuPrereqBuchstab.roughCount (ε * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd)
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs_cofactor_nat_div_cast {N p m : ℕ} {ε z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) (hpm : (p, m) ∈ goldbachG11RoughPairs N ε v) :
    (N - p) / goldbachG11LabelProd v = m ∧ ↑((N - p) / goldbachG11LabelProd v) = ↑(N - p) / ↑(goldbachG11LabelProd v) ∧ ↑(N - p) = ↑N - ↑p

    Natural division is exact only after the pair equation supplies divisibility; the subtraction cast is justified by the original finite range.

    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs_mem_window {N p m : ℕ} {ε z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) (hpm : (p, m) ∈ goldbachG11RoughPairs N ε v) :
    m ∈ goldbachG11CofactorWindow N ε v
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CofactorWindow_prime_pair {N m : ℕ} {ε z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) (hm : m ∈ goldbachG11CofactorWindow N ε v) (hp : Nat.Prime (N - goldbachG11LabelProd v * m)) :
    (N - goldbachG11LabelProd v * m, m) ∈ goldbachG11RoughPairs N ε v
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughCount_eq_prime_window {N : ℕ} {ε z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) :
    goldbachG11RoughCount N ε v = ↑{m ∈ goldbachG11CofactorWindow N ε v | Nat.Prime (N - goldbachG11LabelProd v * m)}.card
    Inspect dependencies

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