α : Type u_1
E : Type u_2
F : Type ?u.245931
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 μ
hs : Convex ℝ s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : IsProbabilityMeasure ((↑↑μ univ)⁻¹ • μ)
⊢ (⨍ (x : α), f x ∂μ) ∈ s
α : Type u_1
E : Type u_2
F : Type ?u.245931
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 μ
hs : Convex ℝ s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
⊢ (⨍ (x : α), f x ∂μ) ∈ s
have : IsProbabilityMeasure ((μ univ)⁻¹ • μ) := isProbabilityMeasureSmul hμ
α : Type u_1
E : Type u_2
F : Type ?u.245931
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 μ
hs : Convex ℝ s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : IsProbabilityMeasure ((↑↑μ univ)⁻¹ • μ)
⊢ (↑↑μ univ)⁻¹ • μ ≪ μ
α : Type u_1
E : Type u_2
F : Type ?u.245931
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 μ
hs : Convex ℝ s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : IsProbabilityMeasure ((↑↑μ univ)⁻¹ • μ)
⊢ (⨍ (x : α), f x ∂μ) ∈ s
refine' hs.integral_mem hsc (ae_mono' _ hfs) hfi.to_average
no goals
α : Type u_1
E : Type u_2
F : Type ?u.245931
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 μ
hs : Convex ℝ s
hsc : IsClosed s
hμ : μ ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : IsProbabilityMeasure ((↑↑μ univ)⁻¹ • μ)
⊢ (↑↑μ univ)⁻¹ • μ ≪ μ
exact AbsolutelyContinuous.smul (refl _) _