theorem AnalyticNumberTheory.LargeSieve.aggregateCauchyFactFour : Fact (1 ≤ 4)

theorem AnalyticNumberTheory.LargeSieve.piLp_four_norm_pow {ι : Type u_1} [Fintype ι] (v : PiLp 4 fun (x : ι) => ℂ) : ‖v‖ ^ 4 = ∑ i : ι, ‖v.ofLp i‖ ^ 4

theorem AnalyticNumberTheory.LargeSieve.aggregate_cauchy_fourth {ι : Type u_1} [Fintype ι] (f : ι → ℂ → ℂ) (s : ℂ) (r B : ℝ) (hr : 0 < r) (hB : 0 ≤ B) (hf : ∀ (i : ι), Differentiable ℂ (f i)) (hcircle : ∀ z ∈ Metric.sphere s r, ∑ i : ι, ‖f i z‖ ^ 4 ≤ B) : ∑ i : ι, ‖deriv (f i) s‖ ^ 4 ≤ B / r ^ 4

Apply Banach-valued Cauchy once in the finite ℓ⁴ space, not separately and then bound each coordinate by the entire family. No cardinality loss.

theorem AnalyticNumberTheory.LargeSieve.aggregate_weighted_cauchy_fourth {ι : Type u_1} [Fintype ι] (f : ι → ℂ → ℂ) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (s : ℂ) (r B : ℝ) (hr : 0 < r) (hB : 0 ≤ B) (hf : ∀ (i : ι), Differentiable ℂ (f i)) (hcircle : ∀ z ∈ Metric.sphere s r, ∑ i : ι, w i * ‖f i z‖ ^ 4 ≤ B) : ∑ i : ι, w i * ‖deriv (f i) s‖ ^ 4 ≤ B / r ^ 4

Nonnegative scalar weights are absorbed in the ℓ⁴ coordinates before Cauchy.