OneSidedCharacterBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The one-sided bound on an explicitly partitioned long-variable range

def OAI.Ostmann.progressionCorrelationWeight line 14
Source documentation
The actual correlation weight on one interval/residue piece. Values outside the piece are set to zero only to state finite variation on ℕ.
```
noncomputable def progressionCorrelationWeight {A I B : Type*} (N : I → ℕ)
    (e : A ≃ Σ i, Fin (N i)) (η : A → ℝ) (W : B → A → ℂ)
    (q r : B) (i : I) (j : ℕ) : ℂ :=
…
```
theorem OAI.Ostmann.partitioned_character_correlation line 22

theorem OAI.Ostmann.one_sided_character_bound line 61

Source documentation

All off-diagonal correlations are derived from exact progression cancellation. Irregular unary restrictions remain in U and V.

theorem one_sided_character_bound {A I : Type*} [Fintype A] [Fintype I]
    (Q : Finset ℕ) (hprime : ∀ q ∈ Q, q.Prime)
    (χ : ∀ q : Q, DirichletCharacter ℂ (q : ℕ)) (hnonprincipal : ∀ q, χ q ≠ 1)
    (N a M : I → ℕ) (e : A ≃ Σ i, Fin (N i)) (value : A → ℕ)
    (hvalue : ∀ i (j : Fin (N i)), value (e.symm ⟨i, j⟩) = a i + M i * j.val)
    (hM : ∀ i (q : Q), (M i).Coprime (q : ℕ))
    (μ η : A → ℝ) (ν : Q → ℝ) (U : A → ℂ) (V : Q → ℂ) (W : Q → A → ℂ)
    (C α H B Z : ℝ) (Bq : ℕ) (hC : 0 ≤ C) (hα : 0 ≤ α) (hH : 0 ≤ H) (hZ : 0 ≤ Z)
    (hμ : ∀ p, 0 ≤ μ p) (hmassμ : ∑ p, μ p ≤ 1)
    (hdom : ∀ p, μ p ≤ C * η p) (hη : ∀ p, 0 ≤ η p) (hmassη : ∑ p, η p ≤ H)
    (hν : ∀ q, 0 ≤ ν q) (hmassν : ∑ q, ν q ≤ 1) (hatom : ∀ q, ν q ≤ α)
    (hU : ∀ p, ‖U p‖ ≤ 1) (hV : ∀ q, ‖V q‖ ≤ 1)
…