PPTSurvivingSlack.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The comparison simplex after a maximal-prefix choice and cancellation. The surviving coordinates retain their order, so their smaller renewal weights preserve the actual inverse-cube row margin. Grid and normality errors are charged explicitly to this margin.

lemma OAI.TotientAsymptotic.ppt_fin_embedding_offset line 18
lemma OAI.TotientAsymptotic.ppt_sum_positive_fin_indices line 36

lemma OAI.TotientAsymptotic.ppt_surviving_row_sum_le line 59

Source documentation

Removing ordered coordinates decreases the renewal-weighted row.

lemma ppt_surviving_row_sum_le {b n : ℕ} (ι : Fin b ↪o Fin n)
    (hb : 0 < b) (v : Fin n → ℝ) (hv : ∀ j, 0 ≤ v j) :
    (∑ r : Fin b, if 0 < r.val then a r.val*v (ι r) else 0) ≤
      ∑ j : Fin n, if ι ⟨0,hb⟩ < j then
        a (j.val-(ι ⟨0,hb⟩).val)*v j else 0 := by
…

Mentions: OAI.TotientAsymptotic.a

lemma OAI.TotientAsymptotic.ppt_gridded_surviving_row line 102

Source documentation

The actual order embedding supplies the reindexing, while each grid coordinate pays only its stated additive error.

lemma ppt_gridded_surviving_row {b n : ℕ} (ι : Fin b ↪o Fin n)
    (hb : 0 < b) (v : Fin n → ℝ) (ν : ℕ → ℝ) {T σ e : ℝ}
    (hT : 0 < T) (hv : ∀ j, 0 ≤ v j)
    (hrow : (∑ j : Fin n, if ι ⟨0,hb⟩ < j then
      a (j.val-(ι ⟨0,hb⟩).val)*v j else 0) ≤ (1-σ)*T)
    (hgrid : ∀ r : Fin b, 0 < r.val → ν r.val ≤ v (ι r)/T+e) :
    (∑ r ∈ Finset.Icc 1 (b-1), a r*ν r) ≤
      1-σ+e*(∑ r ∈ Finset.Icc 1 (b-1), a r) := by
…

Mentions: OAI.TotientAsymptotic.a

theorem OAI.TotientAsymptotic.ppt_relaxed_surviving_slack line 143

Source documentation

The inverse-cube margin comes from membership in the constructed geometric family, before matching coordinates are removed.

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

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

theorem OAI.TotientAsymptotic.ppt_relaxed_surviving_exponent line 158

Source documentation

After charging the grid widths and normality discrepancy, the published comparison exponent retains half the concrete row margin.

theorem ppt_relaxed_surviving_exponent {m n b : ℕ} {budget c T headError e w S z : ℝ}
    {v : Fin n → ℝ} (hv : v ∈ relaxedGeometricFamily m n budget c)
    (ι : Fin b ↪o Fin n) (hb : 0 < b) (ν μ : ℕ → ℝ)
    (hT : 0 < T) (hBz : B z ≠ 0)
    (hhead : v (ι ⟨0,hb⟩) ≤ T+headError)
    (herr : 4*headError ≤
      (rowContractionError (m-((ι ⟨0,hb⟩).val+1))/2)*T)
    (hgrid : ∀ r : Fin b, 0 < r.val → ν r.val ≤ 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-((ι ⟨0,hb⟩).val+1))/16) :
…

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