PPTRowMargin.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The relaxed geometric family retains the row and adjacent-coordinate margins required by the PPT comparison construction. A bounded change of the normalizing head coordinate consumes only part of that margin.

lemma OAI.TotientAsymptotic.ppt_half_row_error_bounds line 17
lemma OAI.TotientAsymptotic.ppt_row_budget_after_head_error line 29

theorem OAI.TotientAsymptotic.ppt_relaxed_row_budget line 43

Source documentation

The explicit inverse-cube row budget is retained under a head error of at most a quarter of the relaxed row margin.

theorem ppt_relaxed_row_budget {m n : ℕ} {B c T e : ℝ} {v : Fin n → ℝ}
    (hv : v ∈ relaxedGeometricFamily m n B c) (i : Fin n)
    (hT : 0 < T) (hhead : v i ≤ T+e)
    (herr : 4*e ≤ (rowContractionError (m-(i.val+1))/2)*T) :
    (∑ j : Fin n, if i < j then a (j.val-i.val)*v j else 0) ≤
      (1-rowContractionError (m-(i.val+1))/8)*T := by
…

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

theorem OAI.TotientAsymptotic.ppt_relaxed_top_budget line 55
lemma OAI.TotientAsymptotic.ppt_normalized_contracted_coordinate line 65

theorem OAI.TotientAsymptotic.ppt_relaxed_first_cutoff_loss line 87

Source documentation

The pairwise margin of the actual relaxed family supplies the first-cutoff condition once head and grid errors fit in its budget.

theorem ppt_relaxed_first_cutoff_loss {m n : ℕ} {B c T e η ν : ℝ}
    {v : Fin n → ℝ} (hv : v ∈ relaxedGeometricFamily m n B c)
    (i j : Fin n) (hij : i < j) (hT : 0 < T) (he : 0 ≤ e)
    (hhead : v i ≤ T+e) (hν : ν ≤ v j/T+η)
    (herr : 4*(e/T+η) ≤ rowContractionError (m-(i.val+1))/2)
    (hbudget : 4*Real.log (10*T) ≤ T*(rowContractionError (m-(i.val+1))/2)) :
    Real.log (10*T) ≤ T*(1-ν) := by
…

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