TupleCoefficient.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual tuple count approximates the finite arithmetic coefficient.

def OAI.TotientAsymptotic.tupleNormalization line 14
Distinct definitions of this name: ComparatorChallenges/TotientAsymptotic.lean:116 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.tupleNormalization@path.
lemma OAI.TotientAsymptotic.tupleNormalization_pos line 16
theorem OAI.TotientAsymptotic.tuple_mass_normalized_approximation line 22
Source documentation
The largest-prime summation error tends to zero for each fixed cutoff, uniformly over all bounded weights and all comparable endpoints.
```
theorem tuple_mass_normalized_approximation (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    {a : ℝ} (ha : 0 < a) :
    ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
      ∀ t : ℝ, a*x ≤ t → t ≤ x → ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      |weightedTupleCount x H t f/tupleNormalization x-(t/x)*(M x H f/G x (m x))| ≤ ε := by
…
```
Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.weightedTupleCount, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m
theorem OAI.TotientAsymptotic.tuple_finite_coefficient_approximation line 63
Source documentation
Combining the proved prime summation with the proved mass/volume bridge leaves only the distinct-value/collision argument. This is a theorem about actual tuples, not a published hypothesis.
```
theorem tuple_finite_coefficient_approximation (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hmertens : MertensProductInput)
    (hren : FordRenewalInput) (hford : FordCoordinateConcentrationInput)
    {a : ℝ} (ha : 0 < a) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, a*x ≤ t → t ≤ x →
        |weightedTupleCount x H t f/tupleNormalization x-(t/x)*AH H f (theta x)| ≤ δ H+ε := by
…
```
Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.weightedTupleCount, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.theta