BinLabels.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative bin labels and real interpolation

The count in a finite prime bin includes multiplicity. Its additivity gives complete multiplicativity of the uncentered labels. Centering is performed only after evaluating a label; no multiplicativity is claimed for it.

A tensor product of finite Vandermonde inverses expresses every function of bounded count vectors as a fixed finite linear combination of real, nonnegative, 1-bounded multiplicative interpolants.

def OAI.JointDickman.primeBin line 27
Source documentation
The prime bin (x^(k/J), x^((k+1)/J)].
```
noncomputable def primeBin (x : ℝ) (J k : ℕ) : Finset ℕ := by
…
```
def OAI.JointDickman.binCount line 32
Source documentation
The number of factors in a finite bin, with multiplicity.
```
def binCount (E : Finset ℕ) (n : ℕ) : ℕ := ∑ p ∈ E, n.factorization p
```
theorem OAI.JointDickman.binCount_one line 34
theorem OAI.JointDickman.binCount_zero line 37
theorem OAI.JointDickman.binCount_mul line 40
theorem OAI.JointDickman.binCount_eq_zero_of_no_factor line 44
def OAI.JointDickman.binLabel line 53
Source documentation
A bin label, viewed as an arithmetic function (so its value at zero is zero).
```
noncomputable def binLabel (E : ι → Finset ℕ) (z : ι → R) : ArithmeticFunction R :=
…
```
theorem OAI.JointDickman.binLabel_apply_zero line 56
theorem OAI.JointDickman.binLabel_apply line 59
theorem OAI.JointDickman.binLabel_apply_one line 62
theorem OAI.JointDickman.binLabel_mul line 66
Source documentation
Complete multiplicativity, without a coprimality requirement.
```
theorem binLabel_mul (E : ι → Finset ℕ) (z : ι → R) (m n : ℕ) :
    binLabel E z (m * n) = binLabel E z m * binLabel E z n := by
…
```
Mentions: OAI.JointDickman.binLabel
theorem OAI.JointDickman.binLabel_isMultiplicative line 75
theorem OAI.JointDickman.binLabel_eq_one_of_no_factor line 79
theorem OAI.JointDickman.binLabel_mul_invariant line 87
theorem OAI.JointDickman.binLabel_nonneg line 98
theorem OAI.JointDickman.binLabel_le_one line 105
theorem OAI.JointDickman.abs_binLabel_le_one line 113
theorem OAI.JointDickman.norm_binLabel_eq_one line 118
theorem OAI.JointDickman.norm_binLabel_le_one line 122
theorem OAI.JointDickman.norm_centered_binLabel_le_two line 128
theorem OAI.JointDickman.centered_binLabel_mul_invariant line 135
theorem OAI.JointDickman.primeBin_eventually_no_factor line 144
Source documentation
A fixed nonzero integer eventually has no factor in any of the large-prime bins. The first bin index is at least one, as in the manuscript.
```
theorem primeBin_eventually_no_factor {ι : Type*} (J : ℕ) (hJ : 0 < J)
    (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i) {u : ℕ} (hu : u ≠ 0) :
    ∀ᶠ x : ℝ in Filter.atTop, ∀ i p, p ∈ primeBin x J (k i) → ¬p ∣ u := by
…
```
Mentions: OAI.JointDickman.primeBin

theorem OAI.JointDickman.binLabel_eventually_mul_invariant line 161

Source documentation

The exact eventual multiplier invariance used for uncentered labels.

theorem binLabel_eventually_mul_invariant {ι R : Type*} [Fintype ι] [CommMonoidWithZero R]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (z : ι → R) {u : ℕ} (hu : u ≠ 0) :
    ∀ᶠ x : ℝ in Filter.atTop, ∀ n : ℕ,
      binLabel (fun i => primeBin x J (k i)) z (u * n) =
        binLabel (fun i => primeBin x J (k i)) z n := by
…

Mentions: OAI.JointDickman.binLabel, OAI.JointDickman.primeBin

def OAI.JointDickman.interpolationNode line 176
Source documentation
Distinct real interpolation nodes strictly between zero and one.
```
noncomputable def interpolationNode {m : ℕ} (j : Fin m) : ℝ := ((j : ℝ) + 1) / ((m : ℝ) + 1)
```
theorem OAI.JointDickman.interpolationNode_pos line 178
theorem OAI.JointDickman.interpolationNode_mem line 182
theorem OAI.JointDickman.interpolationNode_injective line 191
theorem OAI.JointDickman.tensor_inverse_identity line 199

theorem OAI.JointDickman.exists_bounded_count_interpolation line 230

Source documentation

Finite tensor interpolation for arbitrary tables on bounded count vectors.

theorem exists_bounded_count_interpolation {m : ℕ} (v : Fin m → ℝ)
    (hv : Function.Injective v) (F : (ι → Fin m) → ℂ) :
    ∃ c : (ι → Fin m) → ℂ, ∀ t : ι → Fin m,
      F t = ∑ a : ι → Fin m, c a * ∏ i, (v (a i) : ℂ) ^ ((t i : Fin m) : ℕ) := by
…

theorem OAI.JointDickman.centered_binLabel_interpolation line 262

Source documentation

A centered phase label on bounded count vectors is a fixed finite linear combination of real multiplicative interpolants with nodes in [0,1].

theorem centered_binLabel_interpolation (ζ : ι → ℂ) (μ : ℂ) (J : ℕ) :
    ∃ c : (ι → Fin (J + 1)) → ℂ, ∀ E : ι → Finset ℕ, ∀ n : ℕ, n ≠ 0 →
      (∀ i, binCount (E i) n ≤ J) →
      binLabel E ζ n - μ = ∑ a : ι → Fin (J + 1),
        c a * (binLabel E (fun i => interpolationNode (a i)) n : ℂ) := by
…

Mentions: OAI.JointDickman.binCount, OAI.JointDickman.binLabel, OAI.JointDickman.interpolationNode