PrimeFamilyWeights.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Tuple weights in integer and product residue environments.

def OAI.TwoPointCorrelations.familyCenter line 17
Source documentation
An arbitrary offset for every prime coordinate includes all product residue environments. The integer environment has every offset equal to zero.
```
noncomputable def familyCenter (value : (i : α) → P i → ℕ)
    (offset : (i : α) → P i → ℤ) (x : (i : α) → P i) (n : ℤ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.familyTuple line 21
lemma OAI.TwoPointCorrelations.familyCenter_abs line 25
lemma OAI.TwoPointCorrelations.familyCenter_abs_le_one line 32
lemma OAI.TwoPointCorrelations.familyCenter_padding_periodic line 45

theorem OAI.TwoPointCorrelations.familyCenter_square_sum_le line 58

Source documentation

The exact degree estimate, uniform over all residue offsets.

theorem familyCenter_square_sum_le (value : (i : α) → P i → ℕ)
    (hprime : ∀ i p, (value i p).Prime)
    (offset : (i : α) → P i → ℤ) (n : ℤ) (W : ℝ)
    (hV : ∀ i, ∑ p, (value i p : ℝ)⁻¹ ≤ 2 * W)
    (hdegree : (∑ i, ∑ p : P i, if (value i p : ℤ) ∣ offset i p + n then (1 : ℝ) else 0) ≤
      6 * W * Fintype.card α) :
    (∑ x : (i : α) → P i, |familyCenter value offset x n| ^ 2) ≤
      (8 * W) ^ Fintype.card α := by
…

Mentions: OAI.TwoPointCorrelations.familyCenter

lemma OAI.TwoPointCorrelations.familyTuple_primeFactors line 78
lemma OAI.TwoPointCorrelations.familyCenter_zero_eq_centeredTuple line 96
Source documentation
With distinct selected primes, the integer family center is exactly the paper's product over prime divisors of the numerical tuple.
```
lemma familyCenter_zero_eq_centeredTuple (value : (i : α) → P i → ℕ)
    (hprime : ∀ i p, (value i p).Prime) (x : (i : α) → P i)
    (hinj : Function.Injective (fun i => value i (x i))) (n : ℤ) :
    familyCenter value (fun _ _ => 0) x n = centeredTuple (familyTuple value x).primeFactors n := by
…
```
Mentions: OAI.TwoPointCorrelations.familyCenter, OAI.TwoPointCorrelations.centeredTuple, OAI.TwoPointCorrelations.familyTuple