OAI/NumberTheory/TotientAsymptotic/PrefixRelaxation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.prefixRegion_subset_relaxation line 14
2. theorem OAI.TotientAsymptotic.prefix_relaxation_volume_bound line 22

   Source documentation

   Relaxing several inequalities at once costs their sum with the exact renewal weights. This avoids multiplying an error by the dimension.

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

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

3. def OAI.TotientAsymptotic.prefixBandRegion line 54
4. def OAI.TotientAsymptotic.prefixPerturbation line 58
5. def OAI.TotientAsymptotic.topPerturbation line 61
6. lemma OAI.TotientAsymptotic.xi_sub_one_pos line 63
7. lemma OAI.TotientAsymptotic.bandScale_nonneg line 68
8. lemma OAI.TotientAsymptotic.prefixPerturbation_nonneg line 73
9. lemma OAI.TotientAsymptotic.topPerturbation_nonneg line 78
10. lemma OAI.TotientAsymptotic.banded_tailRegion_subset_perturbed line 81
11. lemma OAI.TotientAsymptotic.perturbed_banded_subset_relaxation line 94