PPTHeadResidualFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original-head residual case uses the top simplex inequality. Only the surviving tail coordinates embed in the geometric vector; the first prime is handled by the normal large-part condition.

theorem OAI.TotientAsymptotic.ppt_head_pair_exponent line 19

Source documentation

The true top-row exponent saving, including the empty surviving-tail case b = 1. The head is not embedded in the tail vector.

theorem ppt_head_pair_exponent {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n b H : ℕ) (budget c S e w δ : ℝ)
      (t : ShiftedPair b) (v : Fin n → ℝ) (ι : Fin (b-1) ↪o Fin n) (ν μ : ℕ → ℝ),
      ∀ hb : 0 < b,
      v ∈ relaxedGeometricFamily m n budget c → (∀ i, 3 ≤ t.left i) →
      budget ≤ B z+1 →
      (∀ r : Fin (b-1), v (ι r) = B (t.left ⟨r.val+1,by omega⟩)) →
      1 ≤ H → b ≤ H → m+1 ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      0 ≤ δ → δ ≤ 2*((Real.log (B z))^5/Real.sqrt (B z)) →
      e ≤ (2*(b : ℝ)+4)*δ → w ≤ (4*(b : ℝ)+3)*δ → Real.sqrt (B S/B z) ≤ δ →
      (∀ i : Fin b, 0 < i.val → ν i ≤ B (largestPrimeFactor (t.left i-1))/B z+e) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_head_residual_block_decay line 67
Source documentation
An original-head residual family has the saved comparison bound from its actual prime lists and geometric rows. The explicit arithmetic conditions are supplied after the square and nonnormal preimages have been removed. No comparison-condition or exponent conclusion is an assumption of this application theorem.
```
theorem ppt_head_residual_block_decay (d : ℕ) (hd : 0 < d)
    {A : ℝ} (hA : 0 < A) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m N b h H c a : ℕ) (budget g W V e w δ : ℝ) (ν μ : ℕ → ℝ)
      (tail : Fin h → ℕ) (T : Finset ℕ) (t : ℕ → ShiftedPair b),
      ∀ hb : 1 ≤ b, 1 ≤ H → b ≤ H → h ≤ H → m+1 ≤ H →
      budget ≤ B z+1 → (H : ℝ) ≤ A*Real.log (B z) →
      1 < W → 0 ≤ B W → W ≤ V → W ≤ z →
      B (comparisonCutoffs z ν b) ≤ 2*(B z)^(2/3 : ℝ) →
      0 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      a = ∏ i, tail i → Function.Injective tail →
      (∀ i, IsNormalPrime W (tail i)) →
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.IsNormalPrime