PrimeDivisorEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The low-weight coefficient energy of the actual divisor sums

def OAI.Ostmann.primeDivisorQuadratic line 11
theorem OAI.Ostmann.primeDivisorQuadratic_pair line 20

theorem OAI.Ostmann.primeDivisor_quadratic_energy line 53

Source documentation

The unweighted coefficient-energy bound obtained from double-divisor correlations for the quadratic family.

theorem primeDivisor_quadratic_energy (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (S : ∀ p : ℕ, Finset (ZMod p)) (W : Finset ℕ → Finset ℕ)
    (a : ∀ U : Finset ℕ, ZMod U.toList.prod) (θ : Finset ℕ → ℝ)
    (Φ : 𝓢(ℝ, ℂ)) (R v C lam : ℝ) (M N : ℕ) (c : Finset ℕ → ℂ)
    (hR : 0 < R) (hv : 0 < v) (hC : 0 ≤ C) (hlam : 0 ≤ lam)
    (hM : 0 < M) (hN : 0 < N) (hperiod : P.toList.prod ^ 2 ≤ N)
    (hW : ∀ Q ⊆ P, ∀ w ∈ W Q,
      0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * Q.toList.prod / ((N : ℝ) * v))
    (hc : ∀ U ∈ P.powerset, ‖c U‖ ≤ lam ^ U.card) :
    (∑ n ∈ Finset.range N, (1 / ((n + M : ℕ) : ℝ)) *
      ‖∑ U ∈ P.powerset, c U * primeDivisorQuadratic P hP S W a θ Φ R v U (n + M)‖ ^ 2) ≤
      (C * (4 * correlationWeightBudget Φ Φ C C)) *
…

Mentions: OAI.Ostmann.primeDivisorQuadratic, OAI.Ostmann.correlationWeightBudget

theorem OAI.Ostmann.primeDivisor_low_weight_energy line 79

Source documentation

Low-weight indices may be restricted arbitrarily; positivity extends the underlying energy to the full interval before the divisor expansion.

theorem primeDivisor_low_weight_energy (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (hlarge : ∀ p ∈ P, 10000 ≤ p)
    (S : ∀ p : ℕ, Finset (ZMod p)) (W : Finset ℕ → Finset ℕ)
    (a : ∀ U : Finset ℕ, ZMod U.toList.prod) (θ : Finset ℕ → ℝ)
    (Φ : 𝓢(ℝ, ℂ)) (R v C u K : ℝ) (M N : ℕ) (c : Finset ℕ → ℂ) (F : Finset ℕ)
    (hK : (P.card : ℝ) ≤ K)
    (hR : 0 < R) (hv : 0 < v) (hC : 0 ≤ C) (hM : 0 < M) (hN : 0 < N)
    (hperiod : P.toList.prod ^ 2 ≤ N)
    (hW : ∀ Q ⊆ P, ∀ w ∈ W Q,
      0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * Q.toList.prod / ((N : ℝ) * v))
    (hc : ∀ U ∈ P.powerset, ‖c U‖ ≤ (1 / 16 : ℝ) ^ U.card)
    (hF : F ⊆ Finset.range N)
…