AdditiveShell.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Slice bounds for the additive enlargement needed by banded witness boxes.

lemma OAI.TotientAsymptotic.pow_budget_bound line 14
lemma OAI.TotientAsymptotic.pow_budget_pred_bound line 27

theorem OAI.TotientAsymptotic.additive_slack_shell_bound line 37

Source documentation

A single slack slice has its usual linear slice cost even in the additively enlarged simplex.

theorem additive_slack_shell_bound {x : ℝ} {N : ℕ} (hB : 0 < B x) (hN : 0 < N)
    (δ₀ : ℝ) (δ : Fin N → ℝ) (hδ₀ : 0 ≤ δ₀) (hδ : ∀ i, 0 ≤ δ i)
    (i : Fin N) {t : ℝ} (ht : 0 ≤ t) :
    volume.real (prefixRegion N (B x+δ₀) 0 (-δ) \
      prefixRegion N (B x+δ₀) 0 (raiseThreshold (-δ) i t)) ≤
      (t*N*g (i.val+1)/B x)*
        Real.exp ((N : ℝ)/B x*(δ₀+∑ j, g (j.val+1)*δ j))*G x N := by
…

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

theorem OAI.TotientAsymptotic.additive_top_shell_bound line 69

Source documentation

The top-budget slice obeys the same estimate, with coefficient one.

theorem additive_top_shell_bound {x : ℝ} {N : ℕ} (hB : 0 < B x) (hN : 0 < N)
    (δ₀ : ℝ) (δ : Fin N → ℝ) (hδ₀ : 0 ≤ δ₀) (hδ : ∀ i, 0 ≤ δ i)
    {t : ℝ} (ht : 0 ≤ t) :
    volume.real (prefixRegion N (B x+δ₀) 0 (-δ) \
      prefixRegion N (B x+δ₀-t) 0 (-δ)) ≤
      (t*N/B x)*Real.exp ((N : ℝ)/B x*(δ₀+∑ j, g (j.val+1)*δ j))*G x N := by
…

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