no goals
α : Type u_1
E : Type u_2
F : Type ?u.1581214
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
hgi : Integrable (g ∘ f)
⊢ g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
simpa only [average_eq_integral] using
  hg.map_average_le hgc hsc (IsProbabilityMeasure.ne_zero μ) hfs hfi hgi