CenterDegree.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Degree control for products of prime centers

The argument is uniform in the indicators, so it applies both to integer residues and to independent product residues. One prime is chosen from each family, and the total number of lit prime coordinates controls the sum of squared tuple weights.

lemma OAI.TwoPointCorrelations.nonneg_product_le_power_card line 20
def OAI.TwoPointCorrelations.centerMagnitude line 39
lemma OAI.TwoPointCorrelations.centerMagnitude_nonneg line 42
lemma OAI.TwoPointCorrelations.centerMagnitude_le_one line 45
lemma OAI.TwoPointCorrelations.centerMagnitude_le_indicator_add line 50
lemma OAI.TwoPointCorrelations.center_family_sum_le line 55
lemma OAI.TwoPointCorrelations.squared_center_products_le_product line 62
lemma OAI.TwoPointCorrelations.sum_degree_budget line 88

theorem OAI.TwoPointCorrelations.squared_center_products_le line 101

Source documentation

The sitewise estimate sum_d a_d(n)^2 ≤ (8W)^J, with actual one-prime-per-family products and a total lit-prime degree at most 6WJ.

theorem squared_center_products_le
    {ι : Type*} [Fintype ι] [DecidableEq ι] {P : ι → Type*} [∀ i, Fintype (P i)]
    (θ : (i : ι) → P i → ℝ) (lit : (i : ι) → P i → Bool)
    (W : ℝ)
    (hθ : ∀ i p, 0 ≤ θ i p) (hθ1 : ∀ i p, θ i p ≤ 1)
    (hV : ∀ i, ∑ p, θ i p ≤ 2 * W)
    (hdegree : (∑ i, ∑ p : P i, if lit i p then (1 : ℝ) else 0) ≤
      6 * W * Fintype.card ι) :
    (∑ x : (i : ι) → P i, (∏ i, centerMagnitude (θ i (x i)) (lit i (x i))) ^ 2) ≤
      (8 * W) ^ Fintype.card ι := by
…

Mentions: OAI.TwoPointCorrelations.centerMagnitude