Documentation

MathlibNt.SieveTheory.LiLiuFouvryG9PrefixWeights

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9FirstWeight (N : ℕ) (δ : ℝ) (n : ℕ) :
ℝ

The actual inverse logarithmic weight after eliminating the short box index.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9FirstDenominator_pos {N n : ℕ} {δ : ℝ} (hN : 1 < ↑N) (hδ : δ < 1 / 4) (hn : 0 < n) (hnu : ↑n < ↑N ^ (1 / 10)) :
    0 < (5 / 9 * (1 - Real.log ↑n / Real.log ↑N) - δ) * Real.log ↑N
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9FirstWeight_nonneg {N : ℕ} {ρ δ : ℝ} (hN : 1 < ↑N) (hδ : δ < 1 / 4) {rs : ℕ × ℕ} (hrs : rs ∈ fouvryG9RelaxedPairs N ρ) :
    0 ≤ fouvryG9FirstWeight N δ rs.1
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_log_weight {N : ℕ} {ρ δ : ℝ} (hN : 1 < ↑N) (hρ : 1 < ρ) (hδ : δ < 1 / 4) {k : ℕ × ℕ × ℕ} {n : ℕ} (hn : n ∈ fouvryG9LongShortLabels N ρ k) :
    1 / Real.log (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) ≤ fouvryG9FirstWeight N δ n

    Original Qk, including its buffered 2/3 scale: no replacement level or mask.

    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_log_eq {N n s : ℕ} {ρ : ℝ} (hN : 1 < ↑N) (hρ : 0 < ρ) (hn : 0 < n) (hs : 0 < s) :
    Real.log (ρ ^ 3 * ↑N / (↑n * ↑s)) = Real.log ↑N * (1 + 3 * Real.log ρ / Real.log ↑N - Real.log ↑n / Real.log ↑N - Real.log ↑s / Real.log ↑N)

    Exact prefix logarithm, for the genuinely rho-cubed enlarged product.

    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_kernel_term {N n s : ℕ} {ρ : ℝ} (hN : 1 < ↑N) (hρ : 0 < ρ) (hn : 0 < n) (hs : 0 < s) (δ ζ : ℝ) :
    fouvryG9FirstWeight N δ n * ((1 + ζ) * (ρ ^ 3 * ↑N / (↑n * ↑s)) / Real.log (ρ ^ 3 * ↑N / (↑n * ↑s))) = (1 + ζ) * ρ ^ 3 * ↑N / Real.log ↑N ^ 2 * (1 / (↑n * ↑s * (1 + 3 * Real.log ρ / Real.log ↑N - Real.log ↑n / Real.log ↑N - Real.log ↑s / Real.log ↑N) * (5 / 9 * (1 - Real.log ↑n / Real.log ↑N) - δ)))

    Algebraic assembly into the exact kernel denominator, with no asymptotic loss.

    Inspect dependencies

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