PPTTopSlack.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The comparison exponent for the original large head. Here the remaining surviving coordinates come from the entire geometric tail, so the top simplex budget replaces the row at a later prime.

lemma OAI.TotientAsymptotic.ppt_top_embedding_index line 16
lemma OAI.TotientAsymptotic.ppt_sum_shifted_fin_indices line 32
lemma OAI.TotientAsymptotic.ppt_surviving_top_sum_le line 52
Source documentation
Deletion of arbitrary ordered tail coordinates does not increase the top simplex sum, including when no tail coordinate survives.
```
lemma ppt_surviving_top_sum_le {k n : ℕ} (ι : Fin k ↪o Fin n)
    (v : Fin n → ℝ) (hv : ∀ j, 0 ≤ v j) :
    (∑ r : Fin k, a (r.val+1)*v (ι r)) ≤
      ∑ j : Fin n, a (j.val+1)*v j := by
…
```
Mentions: OAI.TotientAsymptotic.a
lemma OAI.TotientAsymptotic.ppt_gridded_surviving_top line 72

theorem OAI.TotientAsymptotic.ppt_relaxed_surviving_top_slack line 104

Source documentation

The large-head branch uses the original top budget, with the exact same inverse-cube loss after the head normalization error.

theorem ppt_relaxed_surviving_top_slack {m n k : ℕ} {budget c T headError e : ℝ}
    {v : Fin n → ℝ} (hv : v ∈ relaxedGeometricFamily m n budget c)
    (ι : Fin k ↪o Fin n) (ν : ℕ → ℝ)
    (hT : 0 < T) (hhead : budget ≤ T+headError)
    (herr : 4*headError ≤ (rowContractionError m/2)*T)
    (hgrid : ∀ r : Fin k, ν (r.val+1) ≤ v (ι r)/T+e) :
    (∑ r ∈ Finset.Icc 1 k, a r*ν r) ≤
      1-rowContractionError m/8+e*(∑ r ∈ Finset.Icc 1 k, a r) := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.rowContractionError, OAI.TotientAsymptotic.a

theorem OAI.TotientAsymptotic.ppt_relaxed_surviving_top_exponent line 121

Source documentation

This is the exact published exponent for a surviving head outside the tail vector; b = 1 is allowed and has an empty weighted sum.

theorem ppt_relaxed_surviving_top_exponent {m n b : ℕ}
    {budget c T headError e w S z : ℝ} {v : Fin n → ℝ}
    (hv : v ∈ relaxedGeometricFamily m n budget c)
    (ι : Fin (b-1) ↪o Fin n) (ν μ : ℕ → ℝ)
    (hT : 0 < T) (hBz : B z ≠ 0) (hhead : budget ≤ T+headError)
    (herr : 4*headError ≤ (rowContractionError m/2)*T)
    (hgrid : ∀ r : Fin (b-1), ν (r.val+1) ≤ v (ι r)/T+e)
    (hwidth : ∀ r ∈ Finset.Icc 1 (b-1), ν r-μ r ≤ w)
    (herror : e*(∑ r ∈ Finset.Icc 1 (b-1), a r)+2*(b-1 : ℕ)*w+
      Real.sqrt (B S/B z)*(∑ i ∈ Finset.Icc 2 b, ((i : ℝ)*Real.log i+i)) ≤
        rowContractionError m/16) :
    -2+(∑ r ∈ Finset.Icc 1 (b-1),
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.rowContractionError, OAI.TotientAsymptotic.a