DivisorWordMajorant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full divisibility word bound, including exact unlit extra powers.

theorem OAI.TwoPointCorrelations.uniform_divisor_word_reciprocal_bound line 14

Source documentation

Keep the extra power of every designated nonsingleton. The ambient prime pool may contain coordinates unused by the word.

theorem uniform_divisor_word_reciprocal_bound {ι τ : Type*} [Fintype ι] [Fintype τ]
    [DecidableEq ι] (B : ℕ) (p : ι → ℕ) (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (label : τ → ι) (offset : τ → ℤ) (base : ι → Fin B)
    (R H : ℝ) (hR : 0 ≤ R) (hH : 0 < H) (hpH : ∀ i, H ≤ p i)
    (G : (ι → Fin B) → ℝ) (hG : ∀ z, |G z| ≤ 1) :
    |(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)| ≤
      ∑ U ∈ (nonsingletonSlots label).powerset,
        R * (∏ i ∈ univ.image label, (p i : ℝ)⁻¹) * H⁻¹ ^
          (∑ i ∈ nonsingletonLabels label,
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.nonsingletonLabels

lemma OAI.TwoPointCorrelations.designation_card_le_twice_extra line 42
Source documentation
The exact literal number of unlit slots is bounded by twice the retained extra exponent, with no hypothesis about unused coordinates.
```
lemma designation_card_le_twice_extra {ι τ : Type*} [Fintype ι] [Fintype τ]
    [DecidableEq ι] (label : τ → ι) (U : Finset τ) (hU : U ⊆ nonsingletonSlots label) :
    U.card ≤ 2 * ∑ i ∈ nonsingletonLabels label,
      extraReciprocalExponent (litOccurrences label (designationLit U) i).card
        (unlitOccurrences label (designationLit U) i).card := by
…
```
Mentions: OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.extraReciprocalExponent, OAI.TwoPointCorrelations.litOccurrences, OAI.TwoPointCorrelations.designationLit, OAI.TwoPointCorrelations.unlitOccurrences