MinorArcHolder.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite fourth-power Hölder step for the minor-arc cofactor sum.

lemma OAI.TwoPointCorrelations.minor_arc_sum_fourth line 12
lemma OAI.TwoPointCorrelations.minor_arc_weighted_fourth line 25
lemma OAI.TwoPointCorrelations.minor_arc_norm_sum_duality line 38
Source documentation
Polarizing the finite origin sum produces a coefficient of norm one at every origin, including origins where the short sum vanishes.
```
lemma minor_arc_norm_sum_duality (S : Finset ℕ) (f : ℕ → ℂ) :
    ∃ θ : ℕ → ℂ, (∀ k, ‖θ k‖ = 1) ∧
      (∑ k ∈ S, ‖f k‖) = ‖∑ k ∈ S, θ k * f k‖ := by
…
```