AdditiveCost.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Summation of the additive box errors with their exact slice coefficients.

def OAI.TotientAsymptotic.boxErrorTail line 13
lemma OAI.TotientAsymptotic.quadraticShellTail_nonneg line 15
lemma OAI.TotientAsymptotic.boxErrorTail_nonneg line 18
lemma OAI.TotientAsymptotic.boxErrorTail_tendsto line 21
lemma OAI.TotientAsymptotic.cofactor_boxErrorTail_tendsto line 27
lemma OAI.TotientAsymptotic.quadraticShellTail_term line 32
lemma OAI.TotientAsymptotic.boxSlackError_eq line 42
theorem OAI.TotientAsymptotic.uniform_box_error_cost line 47
Source documentation
The total additive error has a tail bound with no dimension factor.
```
theorem uniform_box_error_cost (hren : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H ≤ m x,
      (R x H : ℝ)/B x*(boxTopError x+
        ∑ i : Fin (R x H), g (i.val+1)*boxSlackError x (i.val+1)) ≤ C*boxErrorTail H := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.boxTopError, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.boxSlackError, OAI.TotientAsymptotic.boxErrorTail
theorem OAI.TotientAsymptotic.ambient_box_error_cost line 99
Source documentation
The same retained-coordinate cost with any larger ambient dimension bounded by m; the harmless factor two uses m ≥ 2H.
```
theorem ambient_box_error_cost (hren : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H N : ℕ, 2*H ≤ m x → N ≤ m x →
      (N : ℝ)/B x*(boxTopError x+
        ∑ i : Fin (R x H), g (i.val+1)*boxSlackError x (i.val+1)) ≤ 2*C*boxErrorTail H := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.boxTopError, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.boxSlackError, OAI.TotientAsymptotic.boxErrorTail