PPTFactorLabels.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite label universe for the common prime product and the small left tail. Products are counted as integers. Repeated prime lists only enlarge the reciprocal-mass majorant.

def OAI.TotientAsymptotic.pptPrimeProductFamily line 19
lemma OAI.TotientAsymptotic.mem_pptPrimeProductFamily line 22
lemma OAI.TotientAsymptotic.ppt_prime_product_family_mass line 33
lemma OAI.TotientAsymptotic.ppt_all_factor_lengths_mass line 60
lemma OAI.TotientAsymptotic.ppt_prime_sublist_label line 77
Source documentation
Each prime sublist of a candidate gives an actual label in this finite universe, retaining its exact length.
```
lemma ppt_prime_sublist_label {k N : ℕ} (p : Fin k → ℕ) (I : Finset (Fin k))
    (hp : ∀ i, p i ≤ N ∧ (p i).Prime) :
    (∏ i ∈ I, p i) ∈ pptPrimeProductFamily N I.card := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptPrimeProductFamily

theorem OAI.TotientAsymptotic.ppt_all_residual_label_mass line 95

Source documentation

Common and tail labels together with all lengths, all terminal window indices, and all paired grid labels have a finite explicit mass. No assertion about the number of bad integers enters this bound.

theorem ppt_all_residual_label_mass {A t δ : ℝ} {H N : ℕ}
    (ht0 : 0 < t) (ht : 1 ≤ Real.log t) (hδ : 0 < δ) (hmesh : 1/t ≤ δ)
    (hdim : (H : ℝ) ≤ A*Real.log t) :
    (∑ b ∈ Finset.range (H+1), ∑ _g ∈ collisionGridFamilies δ b,
      ∑ _j ∈ Finset.range (H+1),
      ∑ h ∈ Finset.range (H+1), ∑ a ∈ pptPrimeProductFamily N h,
      ∑ k ∈ Finset.range (H+1), ∑ c ∈ pptPrimeProductFamily N k,
        (a.totient : ℝ)⁻¹*(c.totient : ℝ)⁻¹) ≤
      ((H+1 : ℕ) : ℝ)^4 *
        (max 1 (∑ p ∈ Nat.primesLE N, ((p-1 : ℕ) : ℝ)⁻¹))^(2*H) *
          Real.exp (2*A*(Real.log t)^2) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.collisionGridFamilies, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.pptPrimeProductFamily

theorem OAI.TotientAsymptotic.ppt_residual_labels_exponential_mass line 141

Source documentation

The complete weighted label universe has exponential-square mass at its actual local cutoff. This is the entropy budget consumed by ppt_finite_residual_block_decay.

theorem ppt_residual_labels_exponential_mass {A : ℝ} (hA : 0 ≤ A) :
    ∃ M : ℝ, 0 < M ∧ ∀ᶠ z : ℝ in atTop,
      ∀ (H : ℕ) (δ : ℝ),
        (H : ℝ) ≤ A*Real.log (B z) →
        0 < δ → 1/B z ≤ δ →
        (∑ b ∈ Finset.range (H+1), ∑ _g ∈ collisionGridFamilies δ b,
          ∑ _j ∈ Finset.range (H+1),
          ∑ h ∈ Finset.range (H+1), ∑ a ∈ pptPrimeProductFamily (discardPrimeBound (B z)) h,
          ∑ k ∈ Finset.range (H+1), ∑ c ∈ pptPrimeProductFamily (discardPrimeBound (B z)) k,
            (a.totient : ℝ)⁻¹*(c.totient : ℝ)⁻¹) ≤
          Real.exp (M*(Real.log (B z))^2) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.collisionGridFamilies, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.pptPrimeProductFamily, OAI.TotientAsymptotic.discardPrimeBound