Rectangular sharp hyperbolic prefix maxima with an ambient scale

This leaf separates the endpoint H over which the prefix maximum is taken from the ambient support and damping scale M used by the selector estimate.

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxSquareUpTo (a b : ℤ → ℂ) (H : ℕ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ℝ

The largest squared sharp rectangular hyperbolic prefix norm for 0 ≤ Y ≤ H.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxSquareUpTo a b H Ma Mb Na Nb q χ = (Finset.image (fun (Y : ℕ) => ‖AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicCharacterSum a b Y Ma Mb Na Nb q χ‖ ^ 2) (Finset.range (H + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxAmplitudeUpTo (a b : ℤ → ℂ) (H : ℕ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Square-root amplitude of the maximal squared sharp rectangular prefix up through endpoint H.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxAmplitudeUpTo a b H Ma Mb Na Nb q χ = √(AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxSquareUpTo a b H Ma Mb Na Nb q χ)

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxWeightedPrimitiveMeanUpTo (a b : ℤ → ℂ) (H : ℕ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) : ℝ

Weighted primitive mean in which each character has its own maximizing prefix endpoint bounded by H.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxWeightedPrimitiveMeanUpTo a b H Ma Mb Na Nb S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxAmplitudeUpTo a b H Ma Mb Na Nb q χ

theorem AnalyticNumberTheory.LargeSieve.exists_rectangularSharpHyperbolicPrefixMaxAmplitudeUpTo_eq (a b : ℤ → ℂ) (H : ℕ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ∃ Y ≤ H, rectangularSharpHyperbolicPrefixMaxAmplitudeUpTo a b H Ma Mb Na Nb q χ = ‖rectangularSharpHyperbolicCharacterSum a b Y Ma Mb Na Nb q χ‖

Every maximal squared prefix up to H has an attaining endpoint Y ≤ H, and its square-root amplitude is the norm at that endpoint.

theorem AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicPrefixMaxWeightedPrimitiveMeanUpTo_le (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb Q H M : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (hM : 3 ≤ M) (hHM : H ≤ M) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) (hmnPos : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 0 < m * n) (hmnM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), m * n ≤ ↑M) : rectangularSharpHyperbolicPrefixMaxWeightedPrimitiveMeanUpTo a b H Ma Mb Na Nb S ≤ (1 / 2 + (14 * Real.log ↑M + 4) / Real.pi) * rankOneRectangularLSRHS a b Ma Mb Na Nb Q + 8 / (Real.pi * ↑M) * rectangularCoefficientL1 a b Ma Mb Na Nb * weightedPrimitiveFamilyMass S

Character-wise maximal sharp hyperbolic rectangular primitive L¹ estimate with maximum endpoint H and independent ambient support/damping scale M. Once H ≤ M, the estimate is a direct application of the selector bound, so all constants are measured at M.