Documentation

LeanPool.NairTenenbaum.Arithmetic.MinimalMajorant

The minimal majorant #

Equations (11)–(13) and the submultiplicativity assertion following (13). The paper's max is implemented as a supremum; no attainment is assumed. Including zero makes the definition valid also for the identically zero function.

source
def NairTenenbaum.majorantRatios {k : ℕ} (F : ArithmeticMap k) (m : Tuple k) :
Set ℝ

Ratios used to define G_F, together with zero.

Equations
Instances For
    source
    noncomputable def NairTenenbaum.minimalMajorant {k : ℕ} (F : ArithmeticMap k) (m : Tuple k) :
    ℝ

    Equation (11), with the supremum convention described above.

    Equations
    Instances For
      source
      theorem NairTenenbaum.zero_mem_majorantRatios {k : ℕ} (F : ArithmeticMap k) (m : Tuple k) :
      0 ∈ majorantRatios F m
      source
      theorem NairTenenbaum.majorantRatios_nonempty {k : ℕ} (F : ArithmeticMap k) (m : Tuple k) :
      (majorantRatios F m).Nonempty
      source
      theorem NairTenenbaum.Admissible.ratios_bounded {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (m : Tuple k) (t : ℝ) :
      t ∈ majorantRatios F m → t ≤ growthBound A B ε m
      source
      theorem NairTenenbaum.Admissible.ratios_bddAbove {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (m : Tuple k) :
      BddAbove (majorantRatios F m)
      source
      theorem NairTenenbaum.Admissible.minimalMajorant_nonneg {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (m : Tuple k) :
      0 ≤ minimalMajorant F m
      source
      theorem NairTenenbaum.Admissible.minimalMajorant_le {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (m : Tuple k) :
      minimalMajorant F m ≤ growthBound A B ε m

      Equation (13).

      source
      theorem NairTenenbaum.Admissible.le_minimalMajorant_mul {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (m n : Tuple k) (hmn : Coprime m n) :
      F (m * n) ≤ minimalMajorant F m * F n

      Equation (12), including the case F n = 0.

      source
      theorem NairTenenbaum.minimalMajorant_le_of_bound {k : ℕ} {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (m : Tuple k) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (n : Tuple k), Coprime m n → F (m * n) ≤ C * F n) :
      minimalMajorant F m ≤ C

      G_F is pointwise the least nonnegative factor controlling all coprime translates.

      source
      theorem NairTenenbaum.Admissible.minimalMajorant_submultiplicative {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (a b : Tuple k) (hab : Coprime a b) :
      minimalMajorant F (a * b) ≤ minimalMajorant F a * minimalMajorant F b

      Submultiplicativity of the minimal majorant under coordinatewise coprimality.

      source
      theorem NairTenenbaum.Admissible.minimalMajorant_admissible {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
      Admissible A B ε (minimalMajorant F)

      The assertion G_F ∈ 𝓜ₖ(A,B,ε) following (13).