OAI/NumberTheory/TotientAsymptotic/SimplexTilt.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.simplexDiagonal line 11
2. lemma OAI.TotientAsymptotic.simplexDiagonal_apply line 15
3. lemma OAI.TotientAsymptotic.simplexDiagonal_det line 19
4. def OAI.TotientAsymptotic.positiveSimplex line 23
5. lemma OAI.TotientAsymptotic.positiveSimplex_eq_preimage line 26
6. lemma OAI.TotientAsymptotic.volume_positiveSimplex line 34
7. lemma OAI.TotientAsymptotic.simplex_lower_cap_subset line 49
8. theorem OAI.TotientAsymptotic.volume_simplex_lower_cap_le line 64

   Source documentation

   A finite-dimensional Chernoff bound, before logarithmic estimation.

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

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

9. lemma OAI.TotientAsymptotic.simplex_upper_cap_eq_lower line 77
10. theorem OAI.TotientAsymptotic.volume_simplex_upper_cap_le line 84

    Source documentation

    The corresponding upper-tail volume bound.

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

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