OAI/NumberTheory/TotientAsymptotic/UnbandedPrefixLower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Terminal lower bounds for finite unbanded simplex prefixes.

  1. lemma OAI.TotientAsymptotic.enlargedSimplex_mul_const line 12
  2. lemma OAI.TotientAsymptotic.prefixRegion_last_lower line 34
  3. lemma OAI.TotientAsymptotic.renewal_linear_lower line 65
  4. theorem OAI.TotientAsymptotic.enlarged_prefix_linear_lower line 85

    Source documentation

    The linear lower envelope survives every bounded diagonal enlargement.

    theorem enlarged_prefix_linear_lower : ∃ d : ℝ, 0 < d ∧
    ∀ {N : ℕ} {B β₀ K : ℝ} {β κ u : Fin (N+1) → ℝ},
      0 < K → 0 < β₀ → (∀ i, 0 < β i) →
      (∀ i, 1 ≤ κ i ∧ κ i ≤ K) →
      (∀ i, β₀ ≤ κ i) → (∀ i j, i < j → β i*κ i ≤ κ j) →
      u ∈ enlargedSimplex (N+1) B β₀ β → 1 ≤ u (Fin.last N) →
      ∀ i, d/K*((N+1-i.val:ℕ):ℝ) ≤ u i := by
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.enlargedSimplex