OAI/NumberTheory/TotientAsymptotic/PrefixWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The bounded weights expressing each prefix coordinate in standard-simplex variables.

  1. def OAI.TotientAsymptotic.prefixSimplexMap line 12
  2. def OAI.TotientAsymptotic.prefixWeight line 15
  3. lemma OAI.TotientAsymptotic.prefixSimplexMap_coordinate line 18
  4. lemma OAI.TotientAsymptotic.sum_suffix_weights line 29
  5. lemma OAI.TotientAsymptotic.prefixWeight_nonneg line 47
  6. lemma OAI.TotientAsymptotic.prefixWeight_error line 53
  7. theorem OAI.TotientAsymptotic.prefixWeight_bounds line 64

    Source documentation

    Uniform first- and second-moment bounds; the error is independent of dimension.

    theorem prefixWeight_bounds : ∃ M K : ℝ, 1 ≤ M ∧ 0 < K ∧
    ∀ (N : ℕ) (i : Fin N),
      (∀ j, 0 ≤ prefixWeight N i j ∧ prefixWeight N i j ≤ M) ∧
      |(∑ j, prefixWeight N i j)-(N-i.val:ℕ)| ≤ K ∧
      (∑ j, (prefixWeight N i j)^2) ≤ M*((N-i.val:ℕ)+K) := by
…

    Mentions: OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.prefixWeight