Finite-average forcing lemmas

Generic consequences of an average identity and pointwise nonnegativity.

theorem KasamiCyclicAdditive.forcing_of_average_and_nonneg {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (N Z : ι → ℝ) (c Q : ℝ) (hQ : 0 < Q) (hN : ∀ i ∈ s, N i = c + Z i / Q) (hAV : (∑ i ∈ s, N i) / ↑s.card = c) (hZ : ∀ i ∈ s, 0 ≤ Z i) (i : ι) : i ∈ s → N i = c ∧ Z i = 0

If N i = c + Z i / Q on a nonempty finite index set, the mean of N is c, and Z ≥ 0 pointwise, then N is constantly c and Z vanishes.