OAI/NumberTheory/TotientAsymptotic/SimplexShell.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.pow_sub_positivePart_le line 13
2. def OAI.TotientAsymptotic.raiseThreshold line 26
3. lemma OAI.TotientAsymptotic.weighted_raiseThreshold line 29
4. lemma OAI.TotientAsymptotic.raised_region_subset line 43
5. lemma OAI.TotientAsymptotic.measurableSet_prefixRegion line 55
6. theorem OAI.TotientAsymptotic.prefix_slack_shell_bound line 62

   Source documentation

   Removing a band of thickness t in one slack coordinate loses at most its slice coefficient times t. This holds with every fixed tail threshold.

   theorem prefix_slack_shell_bound {N : ℕ} (hN : 0 < N)
       (B C₀ : ℝ) (C : Fin N → ℝ) (i : Fin N) {t : ℝ} (ht : 0 ≤ t)
       (hT : 0 ≤ B-C₀-∑ j, g (j.val+1)*C j) :
       (volume (prefixRegion N B C₀ C \ prefixRegion N B C₀ (raiseThreshold C i t))).toReal ≤
         (t*N*g (i.val+1)*(B-C₀-∑ j, g (j.val+1)*C j)^(N-1)) /
           ((N.factorial : ℝ)*∏ j : Fin N, g (j.val+1)) := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.raiseThreshold