OAI/NumberTheory/TotientAsymptotic/SimplexCube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every box meeting a basic full prime tuple lies in a controlled multiplicative enlargement of the full simplex.

  1. lemma OAI.TotientAsymptotic.xi_bounds line 16
  2. lemma OAI.TotientAsymptotic.remainderCoord_fin line 22
  3. lemma OAI.TotientAsymptotic.basic_remainder_enlargedSimplex line 27
  4. lemma OAI.TotientAsymptotic.enlargedSimplex_cube line 54

    Source documentation

    Unit-coordinate perturbations of a simplex point are absorbed by the indicated row and budget enlargements.

    lemma enlargedSimplex_cube {N : ℕ} {B β₀ e₀ : ℝ} {β e u v : Fin N → ℝ}
    (hu : u ∈ enlargedSimplex N B β₀ β)
    (hβ : ∀ i, 1 ≤ β i ∧ β i ≤ 2) (hv : ∀ i, 0 ≤ v i)
    (hdist : ∀ i, |u i-v i| ≤ 1)
    (he : ∀ i, ((N-i.val : ℕ) : ℝ)^2+1 ≤ e i*v i)
    (he₀ : (N : ℝ)^2 ≤ e₀*B) :
    v ∈ enlargedSimplex N B (β₀+e₀) (β+e) := by
…

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