Mathlib Jensen for set averages: ConvexOn.map_set_average_le + Even.convexOn_pow

To prove (⨍_{Q} g)^2 ≤ ⨍_{Q} g^2 on a set of finite positive measure, use (Even.convexOn_pow even_two).map_set_average_le (continuous_pow 2).continuousOn isClosed_univ h0 htop (ae_of_all _ fun _ ↦ mem_univ _) hgi hg2i (Mathlib.Analysis.Convex.Integral and Mathlib.Analysis.Convex.Mul). It returns g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ, so the argument order is (convexity, continuity on s, s closed, μ t ≠ 0, μ t ≠ ∞, a.e. f ∈ s, IntegrableOn f, IntegrableOn (g ∘ f)). This saves writing a variance argument by hand. Used it to show |E_{k+1}b - E_k b| ≤ 2^n·β for b in dyadic BMO (L² form).