BinShortAverages.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The real/principal short-average estimate for the actual bin labels

Finite interpolation on fixed windows combines with the published real short-interval input. Real multiplicative weights are allowed, so the result includes the principal-character summands in labels-short.

The weighted long-mean limit remains an explicit arithmetic marginal hypothesis. No short-average estimate, correlation statement, or independence claim is assumed in place of it.

def OAI.JointDickman.weightedBinAverage line 26

Source documentation

The short average of the actual centered bin label with a real weight.

noncomputable def weightedBinAverage {ι : Type*} [Fintype ι]
    (E : ι → Finset ℕ) (ζ : ι → ℂ) (μ : ℂ) (w : ArithmeticFunction ℝ)
    (H z : ℝ) : ℂ :=
…

def OAI.JointDickman.weightedBinInterpolant line 33

Source documentation

The real multiplicative interpolants after multiplying by the real weight.

noncomputable def weightedBinInterpolant {ι : Type*} [Fintype ι]
    (E : ι → Finset ℕ) (w : ArithmeticFunction ℝ) {m : ℕ} (a : ι → Fin m) :
    ArithmeticFunction ℝ :=
…

theorem OAI.JointDickman.weightedBinInterpolant_isMultiplicative line 38
theorem OAI.JointDickman.abs_weightedBinInterpolant_le_one line 43
theorem OAI.JointDickman.finite_average_eq_combination line 52

theorem OAI.JointDickman.weightedBinAverage_eq_combination line 69

Source documentation

Finite-window interpolation gives exact equality of the short sums, including their natural-number-floor endpoint convention.

theorem weightedBinAverage_eq_combination {ι : Type*} [Fintype ι] [DecidableEq ι]
    (E : ι → Finset ℕ) (ζ : ι → ℂ) (μ : ℂ) (w : ArithmeticFunction ℝ) (J : ℕ)
    (c : (ι → Fin (J + 1)) → ℂ) (Y H z : ℝ)
    (hcoeff : ∀ m : ℕ, 1 ≤ m → (m : ℝ) ≤ Y →
      binLabel E ζ m - μ = ∑ a : ι → Fin (J + 1),
        c a * (binLabel E (fun i => interpolationNode (a i)) m : ℂ))
    (hzH : z + H ≤ Y) :
    weightedBinAverage E ζ μ w H z =
      complexShortCombination Finset.univ c (weightedBinInterpolant E w) H z := by
…

Mentions: OAI.JointDickman.binLabel, OAI.JointDickman.interpolationNode, OAI.JointDickman.weightedBinAverage, OAI.JointDickman.weightedBinInterpolant

theorem OAI.JointDickman.weightedBinAverage_eventually_eventually line 95

Source documentation

The principal-character estimate for actual bin labels, conditional only on the published real input and the weighted marginal long-mean limit. The two limits have the manuscript's order: scale first, length second.

theorem weightedBinAverage_eventually_eventually
    (hMR : RealShortIntervalInput)
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (ζ : ι → ℂ) (μ : ℂ)
    (w : ℕ → ArithmeticFunction ℝ) (hwmult : ∀ B, (w B).IsMultiplicative)
    (hw : ∀ B n, |w B n| ≤ 1)
    (A : ℕ → ℝ) (hA : ∀ B, 0 < A B)
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (H : ℕ → ℝ) (hH : Tendsto H atTop atTop)
    (hmarginal : ∀ B, Tendsto
      (fun n => weightedBinAverage (fun i => primeBin (scale n) J (k i)) ζ μ (w B)
…

Mentions: OAI.JointDickman.weightedBinAverage, OAI.JointDickman.primeBin