CofactorWitnessAggregation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal totient weights can be aggregated at fixed cofactor, including tails containing repeated prime factors.

theorem OAI.TotientAsymptotic.cofactor_witness_aggregation line 20

Source documentation

One full-dimensional volume controls a fixed-cofactor witness family. The only arithmetic input is the published prime-box estimate.

theorem cofactor_witness_aggregation (hbox : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {H R a : ℕ} {s : ℝ}, 0 ≤ s → P H ≤ H →
      ∀ (W : Finset (TailDatum H)) (S : TailDatum H → Set (Fin R → ℝ))
        (T : Set (Fin (R+(H-P H)) → ℝ)),
      (∀ η ∈ W, IsWitness H s η) → (∀ η ∈ W, η.cofactor=a) →
      (∀ η ∈ W, MeasurableSet (S η)) → volume T ≠ ⊤ →
      (∀ η ∈ W, ∀ u ∈ S η, ∀ v : Fin (H-P H) → ℝ,
        (∀ i, |tailVector η i-v i| ≤ 1) → joinCoordinates R (H-P H) (u,v) ∈ T) →
      (∑ η ∈ W, ((w η).totient : ℝ)⁻¹*volume.real (S η)) ≤
        (a.totient : ℝ)⁻¹*C*volume.real T := by
…

Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.joinCoordinates, OAI.TotientAsymptotic.w

theorem OAI.TotientAsymptotic.all_cofactor_witness_aggregation line 56

Source documentation

Summing all allowed cofactors retains only the subpolynomial envelope, not the number of witnesses.

theorem all_cofactor_witness_aggregation (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {H R : ℕ} {s : ℝ}, s ∈ Set.Ico (0 : ℝ) 1 → P H ≤ H →
      ∀ (W : Finset (TailDatum H)) (S : TailDatum H → Set (Fin R → ℝ))
        (T : Set (Fin (R+(H-P H)) → ℝ)),
      (∀ η ∈ W, IsWitness H s η) → (∀ η ∈ W, MeasurableSet (S η)) → volume T ≠ ⊤ →
      (∀ η ∈ W, ∀ u ∈ S η, ∀ v : Fin (H-P H) → ℝ,
        (∀ i, |tailVector η i-v i| ≤ 1) → joinCoordinates R (H-P H) (u,v) ∈ T) →
      (∑ η ∈ W, ((w η).totient : ℝ)⁻¹*volume.real (S η)) ≤
        C*Real.exp ((4*(lam/rho))*cofactorScale H)*volume.real T := by
…

Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.joinCoordinates, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.cofactorScale