OAI/NumberTheory/TotientAsymptotic/SimplexExponential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential estimates for linear caps, using only a diagonal volume change.

  1. lemma OAI.TotientAsymptotic.log_one_add_quadratic_lower line 11
  2. lemma OAI.TotientAsymptotic.tilted_product_lower line 21
  3. lemma OAI.TotientAsymptotic.simplex_tilt_power line 37
  4. theorem OAI.TotientAsymptotic.volume_simplex_lower_cap_exp line 50

    Source documentation

    An explicit Chernoff estimate for the lower cap of a uniform simplex.

    theorem volume_simplex_lower_cap_exp (N : ℕ) {B : ℝ} (hB : 0 < B)
    (t s : ℝ) (w : Fin N → ℝ) (hs : 0 ≤ s)
    (hw : ∀ i, -(1/2 : ℝ) ≤ s*w i) (hT : 0 ≤ B+s*t) :
    (volume (standardSimplex N B ∩ {v | (∑ i, w i*v i) ≤ t})).toReal ≤
      Real.exp ((N:ℝ)*(s*t/B)-s*(∑ i, w i)+2*s^2*(∑ i, (w i)^2))*
        (volume (standardSimplex N B)).toReal := by
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.standardSimplex