OAI/NumberTheory/TwoPoint/Bounds/PatternHarmonicSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.representative_weighted_sum line 18

   Source documentation

   Once every occurrence is recovered from its class representative, only one numerical prime per class is summed.

   lemma representative_weighted_sum (F : Finset (ι → P)) (classify : ι → Λ)
       (rep : Λ → ι) (a : P → ℝ) (ha : ∀ p, 0 ≤ a p)
       (hconstant : ∀ w ∈ F, ∀ i, w i = w (rep (classify i))) :
       (∑ w ∈ F, ∏ c, a (w (rep c))) ≤ (∑ p, a p) ^ Fintype.card Λ := by
   …

2. theorem OAI.TwoPointCorrelations.same_pattern_weighted_sum line 40

   Source documentation

   All words in one decoded equality-pattern fiber have the same bound, even though the actual numerical primes vary from word to word.

   theorem same_pattern_weighted_sum (F : Finset (ι → P)) (template : ι → P)
       (a : P → ℝ) (ha : ∀ p, 0 ≤ a p)
       (hpattern : ∀ w ∈ F, ∀ i j, w i = w j ↔ template i = template j) :
       (∑ w ∈ F, ∏ p ∈ univ.image w, a p) ≤
         (∑ p, a p) ^ (univ.image template).card := by
   …

3. theorem OAI.TwoPointCorrelations.same_pattern_reciprocal_sum line 78

   Source documentation

   Specialization to the reciprocal mass of an actual finite prime pool.

   theorem same_pattern_reciprocal_sum (P : Finset ℕ) (F : Finset (ι → P))
       (template : ι → P)
       (hpattern : ∀ w ∈ F, ∀ i j, w i = w j ↔ template i = template j) :
       (∑ w ∈ F, ∏ p ∈ univ.image w, (p.val : ℝ)⁻¹) ≤
         (primeHarmonicMass P) ^ (univ.image template).card := by
   …

   Mentions: OAI.TwoPointCorrelations.primeHarmonicMass

4. theorem OAI.TwoPointCorrelations.covered_pattern_weighted_sum line 89

   Source documentation

   Invalid codes contribute zero. For every valid fiber the reciprocal sum costs one prime mass per observed label, independently of repetitions.

   theorem covered_pattern_weighted_sum {C : Type*} [Fintype C]
       (F : Finset (ι → P)) (decode : C → ι → ι → Bool)
       (a : P → ℝ) (ha : ∀ p, 0 ≤ a p) (M : ℕ)
       (hV : 1 ≤ ∑ p, a p)
       (hlabels : ∀ w ∈ F, (univ.image w).card ≤ M)
       (hcover : ∀ w ∈ F, ∃ c, ∀ i j, decode c i j = decide (w i = w j)) :
       (∑ w ∈ F, ∏ p ∈ univ.image w, a p) ≤
         (Fintype.card C : ℝ) * (∑ p, a p) ^ M := by
   …