ResidualAlignment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Alignment of the two ordered lists of largest factors after prefix cancellation.

theorem OAI.TotientAsymptotic.ordered_largest_factor_alignment_smooth_cutoff line 15

Source documentation

Disjoint decreasing bands turn the factor-count argument into an absolute bound at every paired index. The residual factors are below the lower edge of the prime-factor bands; this edge may be strictly above the normality parameter, as in the application.

theorem ordered_largest_factor_alignment_smooth_cutoff {k D D' : ℕ} (p q : Fin k → ℕ)
    {S Z ε : ℝ} (hSone : 1 < S) (hSZ : S ≤ Z) (hD : D ≠ 0) (hD' : D' ≠ 0)
    (hp : ∀ i, IsNormalPrime S (p i)) (hq : ∀ i, IsNormalPrime S (q i))
    (heq : D*shiftedProduct p = D'*shiftedProduct q)
    (hDs : (largestPrimeFactor D : ℝ) ≤ Z)
    (hD's : (largestPrimeFactor D' : ℝ) ≤ Z)
    (hS : ∀ i, Z ≤ min (largestPrimeFactor (p i-1) : ℝ)
      (largestPrimeFactor (q i-1) : ℝ))
    (hsep : ∀ i j, i < j →
      max (largestPrimeFactor (p j-1) : ℝ) (largestPrimeFactor (q j-1) : ℝ) ≤
      min (largestPrimeFactor (p i-1) : ℝ) (largestPrimeFactor (q i-1) : ℝ))
    (herr : ∀ i, Real.sqrt (B S * B (max (largestPrimeFactor (p i-1) : ℝ)
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.B