OAI/NumberTheory/TotientAsymptotic/SimplexTerminalCap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.simplex_terminal_translate line 12
2. lemma OAI.TotientAsymptotic.volume_simplex_terminal_cap line 48
3. lemma OAI.TotientAsymptotic.simplex_cap_power_bound line 59
4. lemma OAI.TotientAsymptotic.simplex_positive_part_power_bound line 76

   Source documentation

   The exponential bound also covers caps beyond the whole simplex.

   lemma simplex_positive_part_power_bound {B t : ℝ} (hB : 0 < B) (ht : 0 ≤ t)
       {N : ℕ} (hN : 0 < N) :
       (max (B-t) 0)^N ≤ Real.exp (-(N:ℝ)*t/B)*B^N := by
   …

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

5. lemma OAI.TotientAsymptotic.volume_simplex_terminal_cap_le line 85