PhaseSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A numerical subfamily can retain complex mass without cancellation.

lemma OAI.TwoPointCorrelations.coordinate_mass_le line 14
theorem OAI.TwoPointCorrelations.exists_subfamily_complex_mass line 36
Source documentation
Four half-plane selections suffice. The selected family depends only on the numerical coefficients, so it can be used as graph eligibility.
```
theorem exists_subfamily_complex_mass {ι : Type*} (s : Finset ι) (z : ι → ℂ) :
    ∃ t ⊆ s, (∑ i ∈ s, ‖z i‖) / 4 ≤ ‖∑ i ∈ t, z i‖ := by
…
```