PPTLocalValueEnvelope.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Local value and right-preimage prime bounds from the actual candidate prime product. A late residual is controlled by its own coordinate envelope, rather than by the original ambient counting parameter.

def OAI.TotientAsymptotic.pptLocalValueHeight line 17
lemma OAI.TotientAsymptotic.ppt_local_value_height_nonneg line 20

lemma OAI.TotientAsymptotic.ppt_seed_totient_prime_product_log_le line 30

Source documentation

The seed-times-totient value is bounded directly by the sum of the logarithms of the actual primes.

lemma ppt_seed_totient_prime_product_log_le {d n : ℕ} {T : ℝ}
    (hd : 0 < d) (p : Fin n → ℕ) (hp : ∀ i, (p i).Prime)
    (hcoords : ∀ i, B (p i) ≤ T) :
    Real.log ((d*(∏ i, p i).totient : ℕ) : ℝ) ≤
      Real.log (d : ℝ)+(n : ℝ)*Real.exp T := by
…

Mentions: OAI.TotientAsymptotic.B

theorem OAI.TotientAsymptotic.ppt_local_prime_product_value_bound line 49

Source documentation

A product with at most H+1 prime factors has value below the double-exponential endpoint of its local coordinate height.

theorem ppt_local_prime_product_value_bound {d n H : ℕ} {T : ℝ}
    (hd : 0 < d) (hT : 0 ≤ T) (hn : n ≤ H+1)
    (p : Fin n → ℕ) (hp : ∀ i, (p i).Prime)
    (hcoords : ∀ i, B (p i) ≤ T) :
    ((d*(∏ i, p i).totient : ℕ) : ℝ) ≤
      Real.exp (Real.exp (pptLocalValueHeight d H T)) := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptLocalValueHeight

theorem OAI.TotientAsymptotic.ppt_local_preimage_prime_predecessor_bound line 75

Source documentation

Every prime in any preimage of the local value has its predecessor below the same endpoint. This retains all right preimages.

theorem ppt_local_preimage_prime_predecessor_bound {d n H u q : ℕ} {T : ℝ}
    (hd : 0 < d) (hT : 0 ≤ T) (hn : n ≤ H+1)
    (p : Fin n → ℕ) (hp : ∀ i, (p i).Prime)
    (hcoords : ∀ i, B (p i) ≤ T)
    (_hu : 0 < u) (hvalue : u.totient = d*(∏ i, p i).totient)
    (hq : q.Prime) (hqu : q ∣ u) :
    ((q-1 : ℕ) : ℝ) ≤ Real.exp (Real.exp (pptLocalValueHeight d H T)) := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptLocalValueHeight

theorem OAI.TotientAsymptotic.ppt_local_preimage_prime_coordinate_bound line 91

Source documentation

The local sieve for an arbitrary right head can use this endpoint height, up to the harmless predecessor-to-prime error of one.

theorem ppt_local_preimage_prime_coordinate_bound {d n H u q : ℕ} {T : ℝ}
    (hd : 0 < d) (hT : 0 ≤ T) (hn : n ≤ H+1)
    (p : Fin n → ℕ) (hp : ∀ i, (p i).Prime)
    (hcoords : ∀ i, B (p i) ≤ T)
    (hu : 0 < u) (hvalue : u.totient = d*(∏ i, p i).totient)
    (hq : q.Prime) (hq3 : 3 ≤ q) (hqu : q ∣ u) :
    B q ≤ pptLocalValueHeight d H T+1 := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptLocalValueHeight