OAI/NumberTheory/TotientAsymptotic/PerturbationCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The sum of all prefix perturbations, uniformly in dimension and phase.

  1. def OAI.TotientAsymptotic.exponentialShellTail line 14
  2. lemma OAI.TotientAsymptotic.exp_shell_power line 17
  3. lemma OAI.TotientAsymptotic.exponentialShellTail_nonneg line 23
  4. lemma OAI.TotientAsymptotic.exponentialShell_summable line 26
  5. lemma OAI.TotientAsymptotic.exponentialShellTail_term line 33
  6. lemma OAI.TotientAsymptotic.sum_prefix_exponentialShell line 41
  7. theorem OAI.TotientAsymptotic.uniform_prefix_perturbation_cost line 54

    Source documentation

    The relaxation of every prefix inequality has a small total weighted budget. The bound includes index zero and has no dimension factor.

    theorem uniform_prefix_perturbation_cost (hford : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H ≤ m x,
      (R x H : ℝ)/B x*(topPerturbation x+
        ∑ i : Fin (R x H), g (i.val+1)*prefixPerturbation x H i) ≤
        C*exponentialShellTail H := by
…

    Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.topPerturbation, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.prefixPerturbation, OAI.TotientAsymptotic.exponentialShellTail

  8. lemma OAI.TotientAsymptotic.cofactor_exponentialShellTail_tendsto line 120