α : Type u_1
E : Type u_2
F : Type ?u.608928
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✝ : IsFiniteMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
hgi : Integrable (g ∘ f)
ht_mem : ∀ᵐ (x : α) ∂μ, (f x, g (f x)) ∈ {p | p.fst ∈ s ∧ g p.fst ≤ p.snd}
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.fst ∈ s ∧ g p.fst ≤ p.snd}
α : Type u_1
E : Type u_2
F : Type ?u.608928
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✝ : IsFiniteMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
hgi : Integrable (g ∘ f)
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.fst ∈ s ∧ g p.fst ≤ p.snd}
have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
  hfs.mono fun x hx => ⟨hx, le_rfl⟩
no goals
α : Type u_1
E : Type u_2
F : Type ?u.608928
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✝ : IsFiniteMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
hgi : Integrable (g ∘ f)
ht_mem : ∀ᵐ (x : α) ∂μ, (f x, g (f x)) ∈ {p | p.fst ∈ s ∧ g p.fst ≤ p.snd}
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.fst ∈ s ∧ g p.fst ≤ p.snd}
exact average_pair hfi hgi ▸
  hg.convex_epigraph.average_mem (hsc.epigraph hgc) hμ ht_mem (hfi.prod_mk hgi)