PPTComparisonAssembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Assemble the pointwise conditions in Ford's comparison estimate after the actual matched coordinates have been removed. The right residual is an integer multiplier in the shifted-product equation; no additional representation of that multiplier as a totient is required.

def OAI.TotientAsymptotic.pptCanceledPair line 20

theorem OAI.TotientAsymptotic.ppt_canceled_comparison_conditions line 27

Source documentation

The comparison conditions follow from the actual shifted-product identity, target squarefreeness, and the enclosing grid intervals. The large leading part is proved from normality and the head size.

theorem ppt_canceled_comparison_conditions : ∀ᶠ z : ℝ in atTop,
    ∀ (k D E : ℕ) (p q : Fin k → ℕ) (S : ℝ) (Y U : ℕ → ℝ),
      ∀ hk : 0 < k,
      1 < S → 0 ≤ B S → S ≤ z →
      (∀ i, IsNormalPrime S (p i)) → (∀ i, IsNormalPrime S (q i)) →
      Function.Injective p → p ⟨0,hk⟩ ≠ q ⟨0,hk⟩ →
      0 < E → D*shiftedProduct p = E*shiftedProduct q →
      ((D*shiftedProduct p : ℕ) : ℝ) ≤ z →
      SquarefreeAbove (D*shiftedProduct p) (Y (pptUnequalCoordinates p q).card) →
      (largestPrimeFactor E : ℝ) ≤ Y (pptUnequalCoordinates p q).card →
      (∀ i : Fin (pptUnequalCoordinates p q).card,
        U i ≤ largestPrimeFactor (p (pptCoordinateEmbedding p q i)-1) ∧
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.pptUnequalCoordinates, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.pptCoordinateEmbedding

lemma OAI.TotientAsymptotic.ppt_plain_comparison_injective line 76
Source documentation
Left-list recovery alone proves injectivity of a fixed comparison block, even when its right residual is supplied directly as an integer.
```
lemma ppt_plain_comparison_injective {b c a : ℕ} (T : Finset ℕ)
    (t : ℕ → ShiftedPair b)
    (hreal : ∀ n ∈ T, n = c*a*∏ i, (t n).left i) :
    Set.InjOn t (T : Set ℕ) := by
…
```
Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.ShiftedPair

theorem OAI.TotientAsymptotic.ppt_plain_comparison_block_count line 86

Source documentation

The unconditional published estimate on a fixed common-factor and left-tail block, with its actual integer right residual.

theorem ppt_plain_comparison_block_count :
    ∃ C z₀ : ℝ, 0 < C ∧ 1 < z₀ ∧
    ∀ (b d c a : ℕ) (z S : ℝ) (Y U : ℕ → ℝ),
      z₀ ≤ z → FordComparisonParameters b z S (d*a.totient) c.totient Y U →
      ∀ (T : Finset ℕ) (t : ℕ → ShiftedPair b),
        (∀ n ∈ T, n = c*a*∏ i, (t n).left i) →
        (∀ n ∈ T, FordComparisonConditions b z S (d*a.totient) c.totient Y U (t n)) →
        (T.card : ℝ) ≤ fordComparisonBound C b z S (d*a.totient) c.totient Y U := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.FordComparisonParameters, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.FordComparisonConditions, OAI.TotientAsymptotic.fordComparisonBound

theorem OAI.TotientAsymptotic.ppt_plain_normal_tail_comparison_sum line 106

Source documentation

Sum the concrete plain-residual comparison blocks with the proved normal-tail cost, retaining both reciprocal totient masses.

theorem ppt_plain_normal_tail_comparison_sum :
    ∃ C z₀ : ℝ, 0 < C ∧ 1 < z₀ ∧
    ∀ (b d h : ℕ) (z W V : ℝ) (Y U : ℕ → ℝ)
      (R A : Finset ℕ) (T : ℕ → ℕ → Finset ℕ)
      (tail : ℕ → Fin h → ℕ) (t : ℕ → ℕ → ℕ → ShiftedPair b),
      0 < d → z₀ ≤ z → 0 ≤ B z → 1 < W → 0 ≤ B W → W ≤ V → 1 ≤ Y b →
      (∀ a ∈ A, a = ∏ i, tail a i) →
      (∀ a ∈ A, Function.Injective (tail a)) →
      (∀ a ∈ A, ∀ i, IsNormalPrime W (tail a i)) →
      (∀ a ∈ A, ∀ i, (largestPrimeFactor (tail a i-1) : ℝ) ≤ V) →
      (∀ c ∈ R, ∀ a ∈ A,
        FordComparisonParameters b z W (d*a.totient) c.totient Y U) →
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.FordComparisonParameters