PPTLocalDimension.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The geometric lower bound on a remaining prime coordinate bounds the length of that suffix in terms of its own comparison scale. This is a local statement; it does not transfer normality from a larger scale.

def OAI.TotientAsymptotic.pptLocalDimensionConstant line 19
lemma OAI.TotientAsymptotic.ppt_local_dimension_constant_pos line 21
lemma OAI.TotientAsymptotic.ppt_local_dimension_bound line 28
Source documentation
A geometric endpoint lower bound gives a logarithmic local length bound, with a constant depending only on the fixed candidate family.
```
lemma ppt_local_dimension_bound {c t U : ℝ} {H : ℕ}
    (hc : 0 < c) (ht : Real.exp 1 ≤ t)
    (hlower : c*(rho^H)⁻¹ ≤ U) (hupper : U ≤ t+1) :
    (H : ℝ) ≤ pptLocalDimensionConstant c*Real.log t := by
…
```
Mentions: OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.pptLocalDimensionConstant
theorem OAI.TotientAsymptotic.ppt_local_prime_dimension line 62
Source documentation
The endpoint form used for a largest prime in a local comparison block. The harmless +1 comes from replacing p-1 by p.
```
theorem ppt_local_prime_dimension {c : ℝ} (hc : 0 < c) :
    ∀ᶠ z : ℝ in atTop, ∀ (H p : ℕ),
      3 ≤ p → c*(rho^H)⁻¹ ≤ B p → (p-1 : ℕ) ≤ z →
      (H : ℝ) ≤ pptLocalDimensionConstant c*Real.log (B z) := by
…
```
Mentions: OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptLocalDimensionConstant
theorem OAI.TotientAsymptotic.ppt_local_prime_sublist_dimension line 73
Source documentation
Allow the distinguished head prime in addition to the geometric tail length. Every surviving sublist inherits the same local bound.
```
theorem ppt_local_prime_sublist_dimension {c : ℝ} (hc : 0 < c) :
    ∀ᶠ z : ℝ in atTop, ∀ (H p k : ℕ),
      3 ≤ p → c*(rho^H)⁻¹ ≤ B p → (p-1 : ℕ) ≤ z → k ≤ H+1 →
      (k : ℝ) ≤ (pptLocalDimensionConstant c+1)*Real.log (B z) := by
…
```
Mentions: OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptLocalDimensionConstant

lemma OAI.TotientAsymptotic.ppt_local_row_saving line 88

Source documentation

A fixed inverse-cube row margin becomes the inverse-log-cube saving needed by the analytic comparison estimate.

lemma ppt_local_row_saving {c t : ℝ} {H r : ℕ}
    (_ht : 0 < Real.log t) (hrH : r+1 ≤ H)
    (hdim : (H : ℝ) ≤ pptLocalDimensionConstant c*Real.log t) :
    1/(80*(pptLocalDimensionConstant c)^3)/(Real.log t)^3 ≤
      (1/(5*(r+1 : ℝ)^3))/16 := by
…

Mentions: OAI.TotientAsymptotic.pptLocalDimensionConstant

theorem OAI.TotientAsymptotic.ppt_local_head_error_absorbed line 110
Source documentation
A bounded change of head coordinate consumes less than the allowed quarter-row margin, uniformly for every logarithmic local dimension.
```
theorem ppt_local_head_error_absorbed {A E : ℝ} (_hA : 0 < A) (hE : 0 ≤ E) :
    ∀ᶠ t : ℝ in atTop, ∀ H r : ℕ,
      (H : ℝ) ≤ A*Real.log t → r+1 ≤ H →
      4*E ≤ (rowContractionError r/2)*t := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.rowContractionError