The Rademacher convexity inequality

For a finite family of vectors v i and pairwise independent Rademacher signs ε i, each ‖v j‖ is bounded by the expected norm of ∑ i, ε i • v i. Thus the same expectation bounds the maximum of the vector norms. This estimate compares random signed sums with their largest summand, as needed in lower bounds for mean norms of finite-dimensional spaces.

Only pairwise independence is needed: testing the signed sum against a norming functional and multiplying by ε j recovers ‖v j‖ in expectation. No completeness, separability, or finite-dimensionality assumption on the vector space is required. Real scalar multiplication also covers complex normed spaces by restriction of scalars.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §13.3.

theorem Finset.integrable_sum_smul_rademacher {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ι → Ω → ℝ} (s : Finset ι) (v : ι → E) (hε : ∀ i ∈ s, ProbabilityTheory.HasLaw (ε i) TauCeti.Probability.rademacherMeasure P) : MeasureTheory.Integrable (fun (ω : Ω) => ∑ i ∈ s, ε i ω • v i) P

A finite Rademacher sum of fixed vectors is integrable, even in an incomplete space.

theorem Finset.norm_le_integral_norm_sum_smul_rademacher {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ι → Ω → ℝ} (s : Finset ι) (v : ι → E) (hε : ∀ i ∈ s, ProbabilityTheory.HasLaw (ε i) TauCeti.Probability.rademacherMeasure P) (hind : (↑s).Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (ε i) (ε j) P) {j : ι} (hj : j ∈ s) : ‖v j‖ ≤ ∫ (ω : Ω), ‖∑ i ∈ s, ε i ω • v i‖ ∂P

Rademacher convexity inequality. Every summand's norm is bounded by the expected norm of the signed sum. Pairwise independence of the Rademacher signs suffices.

theorem Finset.sup'_norm_le_integral_norm_sum_smul_rademacher {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ι → Ω → ℝ} (s : Finset ι) (hs : s.Nonempty) (v : ι → E) (hε : ∀ i ∈ s, ProbabilityTheory.HasLaw (ε i) TauCeti.Probability.rademacherMeasure P) (hind : (↑s).Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (ε i) (ε j) P) : (s.sup' hs fun (i : ι) => ‖v i‖) ≤ ∫ (ω : Ω), ‖∑ i ∈ s, ε i ω • v i‖ ∂P

The largest norm in a nonempty finite family is bounded by the expected norm of its Rademacher sum.