Aggregating the local determinant exponents for curves

Cauchy–Schwarz preserves the leading quadratic coefficient when residue classes have different multiplicities. These are the numerical aggregation steps in the curve case of CCDN Proposition 2.6. The geometric local divisibility and finite-field multiplicity estimates are not part of this module.

theorem CCDN.aggregate_multiplicity_exponents {ι : Type u_1} (S : Finset ι) (n μ : ι → ℕ) (hμ : ∀ i ∈ S, 0 < μ i) : (∑ i ∈ S, n i) ^ 2 ≤ (2 * ∑ i ∈ S, μ i) * (∑ i ∈ S, multiplicityExponent (n i) (μ i) + ∑ i ∈ S, n i)

Apply the aggregation directly to the repeated local weights.

theorem CCDN.aggregate_exponent_lower {ι : Type u_1} (S : Finset ι) (n μ e : ι → ℕ) (he : ∀ i ∈ S, n i ^ 2 ≤ 2 * μ i * (e i + n i)) {N : ℝ} (hN : 0 < N) (hμ : ↑(∑ i ∈ S, μ i) ≤ N) : ↑(∑ i ∈ S, n i) ^ 2 / (2 * N) - ↑(∑ i ∈ S, n i) ≤ ↑(∑ i ∈ S, e i)

Real-valued form with a uniform upper bound for total residue multiplicity.