OAI/NumberTheory/JointDickman/Arithmetic/WeightedDivisorEdge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.weighted_divisor_edge_reindex line 13

   Source documentation

   Exact transport of a weighted pair, with fixed-multiplier invariance as its only label property. The centered label need not be multiplicative.

   theorem weighted_divisor_edge_reindex {a b c : ℕ}
       (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) {j : ℤ}
       (he : (a : ℤ)-b = j*c) (hcop : a.Coprime j.natAbs)
       (N : ℕ) (w : ℕ → ℝ) (F : ℕ → ℂ)
       (hFa : ∀ n, F (a*n) = F n) (hFb : ∀ n, F (b*n) = F n)
       (hFc : ∀ n, F (c*n) = F n) :
       (∑ m ∈ divisorEdgeOld a b c N,
         w m * (star (F (a*m+1)) * F (b*m+1)).re) =
       ∑ n ∈ divisorEdgeNew a b c N j,
         w (divisorEdgeInverse a b c n) * (star (F n) * F ((n : ℤ)+j).toNat).re := by
   …

   Mentions: OAI.JointDickman.divisorEdgeOld, OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse

2. theorem OAI.JointDickman.centered_movingBinLabel_invariant line 50

   Source documentation

   The required invariances hold for the actual moving centered labels, simultaneously over the fixed auxiliary coefficient family.

   theorem centered_movingBinLabel_invariant {ι : Type*} [Fintype ι]
       (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
       (z : ι → ℂ) (μ : ℂ) (B : ℕ) :
       ∀ᶠ N : ℕ in atTop, ∀ A ∈ (auxiliaryPrimes B).powerset, ∀ n,
         movingBinLabel J k z N ((∏ p ∈ A, p)*n)-μ = movingBinLabel J k z N n-μ := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.movingBinLabel

3. theorem OAI.JointDickman.weighted_binLabel_edge_reindex line 61

   Source documentation

   The exact finite graph reindexing for the manuscript's centered bin labels, with arbitrary real arithmetic weights.

   theorem weighted_binLabel_edge_reindex {ι : Type*} [Fintype ι]
       (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
       (z : ι → ℂ) (μ : ℂ) (B : ℕ) (w : ℕ → ℕ → ℝ) :
       ∀ᶠ N : ℕ in atTop, ∀ A ∈ (auxiliaryPrimes B).powerset,
         ∀ E ∈ (auxiliaryPrimes B).powerset, ∀ D ∈ (auxiliaryPrimes B).powerset,
         ∀ j : ℤ, ((∏ p ∈ A, p : ℕ) : ℤ)-(∏ p ∈ E, p : ℕ) = j*(∏ p ∈ D, p : ℕ) →
         (∏ p ∈ A, p).Coprime j.natAbs →
         (∑ m ∈ divisorEdgeOld (∏ p ∈ A, p) (∏ p ∈ E, p) (∏ p ∈ D, p) N,
           w N m * (star (movingBinLabel J k z N ((∏ p ∈ A, p)*m+1)-μ) *
             (movingBinLabel J k z N ((∏ p ∈ E, p)*m+1)-μ)).re) =
         ∑ n ∈ divisorEdgeNew (∏ p ∈ A, p) (∏ p ∈ E, p) (∏ p ∈ D, p) N j,
           w N (divisorEdgeInverse (∏ p ∈ A, p) (∏ p ∈ E, p) (∏ p ∈ D, p) n) *
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.divisorEdgeOld, OAI.JointDickman.movingBinLabel, OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse