Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuFouvryG9GridIndex

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridIndex (ρ t : ℝ) :
ℕ

Natural logarithmic index, used only for bases greater than one.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridIndex_bounds {ρ t : ℝ} (hρ : 1 < ρ) (ht : 1 ≤ t) :
    ρ ^ fouvryG9GridIndex ρ t ≤ t ∧ t < ρ ^ (fouvryG9GridIndex ρ t + 1)
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridIndex_mono {ρ t N : ℝ} (hρ : 1 < ρ) (ht : 1 ≤ t) (htN : t ≤ N) :
    fouvryG9GridIndex ρ t ≤ fouvryG9GridIndex ρ N
    Inspect dependencies

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