OAI/NumberTheory/TwoPoint/Bounds/ResidueCentering.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.FiniteLaw.average_congr_on_support line 15
2. def OAI.TwoPointCorrelations.forcedResidue line 24
3. lemma OAI.TwoPointCorrelations.forcedResidue_lt line 28
4. lemma OAI.TwoPointCorrelations.divisor_test_iff_forcedResidue line 33
5. theorem OAI.TwoPointCorrelations.uniform_divisor_word_average line 52

   Source documentation

   The equality is needed only on the support of the product law. Values in the common carrier above a coordinate's modulus have zero mass.

   theorem uniform_divisor_word_average {ι τ : Type*} [Fintype ι] [Fintype τ]
       [DecidableEq ι] (B : ℕ) (p : ι → ℕ) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
       (label : τ → ι) (offset : τ → ℤ) (R : ℝ) (G : (ι → Fin B) → ℝ) :
       (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
         (fun z => R * (∏ t,
           ((if (p (label t) : ℤ) ∣ (z (label t)).val + offset t then (1 : ℝ) else 0) -
             (p (label t) : ℝ)⁻¹)) * G z) =
       (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
         (fun z => R * (∏ t,
           ((if z (label t) = forcedResidue B (p (label t)) (hp _) (hpB _) (offset t)
             then (1 : ℝ) else 0) - (p (label t) : ℝ)⁻¹)) * G z) := by
   …

   Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.forcedResidue

6. abbrev OAI.TwoPointCorrelations.ColumnPrimeCoordinate line 70
7. def OAI.TwoPointCorrelations.tupleSlotLabel line 72
8. lemma OAI.TwoPointCorrelations.familyCenter_word_product line 78

   Source documentation

   Flatten the actual product of family centers without changing either the numerical prime labels or their repeated residue coordinates.

   lemma familyCenter_word_product {J R B : ℕ} {P : Fin J → Finset ℕ}
       (w : ColumnPrimeAssignment J R P) (offset : Fin R → ℤ)
       (z : ColumnPrimeCoordinate P → Fin B) :
       (∏ i, familyCenter (fun _ p => p.val)
         (fun j p => ((z ⟨j, p⟩).val : ℤ)) (fun j => w j i) (offset i)) =
         ∏ t : Fin R × Fin J,
           ((if ((tupleSlotLabel w t).2.val : ℤ) ∣
             ((z (tupleSlotLabel w t)).val : ℤ) + offset t.1 then (1 : ℝ) else 0) -
               ((tupleSlotLabel w t).2.val : ℝ)⁻¹) := by
   …

   Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.ColumnPrimeCoordinate, OAI.TwoPointCorrelations.familyCenter, OAI.TwoPointCorrelations.tupleSlotLabel