α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ (⨍ (x : α), f x ∂μ) ∈ interior s
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ (⨍ (x : α), f x ∂μ) ∈ interior s
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s := fun ht =>
  hs.convex.set_average_mem hsc ht (measure_ne_top _ _) (ae_restrict_of_ae hfs) hfi.integrableOn
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
⊢ (∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ (tᶜ) ≠ 0 ∧ (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ) →
    (⨍ (x : α), f x ∂μ) ∈ interior s
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ (⨍ (x : α), f x ∂μ) ∈ interior s
refine' (ae_eq_const_or_exists_average_ne_compl hfi).imp_right _
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
t : Set α
hm : MeasurableSet t
h₀ : ↑↑μ t ≠ 0
h₀' : ↑↑μ (tᶜ) ≠ 0
hne : (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ (⨍ (x : α), f x ∂μ) ∈ interior s
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
⊢ (∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ (tᶜ) ≠ 0 ∧ (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ) →
    (⨍ (x : α), f x ∂μ) ∈ interior s
rintro ⟨t, hm, h₀, h₀', hne⟩
no goals
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.2067161
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 : StrictConvex ℝ s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f
this : ∀ {t : Set α}, ↑↑μ t ≠ 0 → (⨍ (x : α) in t, f x ∂μ) ∈ s
t : Set α
hm : MeasurableSet t
h₀ : ↑↑μ t ≠ 0
h₀' : ↑↑μ (tᶜ) ≠ 0
hne : (⨍ (x : α) in t, f x ∂μ) ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ (⨍ (x : α), f x ∂μ) ∈ interior s
exact
  hs.openSegment_subset (this h₀) (this h₀') hne
    (average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' hfi)