α : Type u_2
E : Type u_1
F : Type ?u.2692874
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✝ : StrictConvexSpace ℝ E
ht : ↑↑μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂Measure.restrict μ t, ‖f x‖ ≤ C
this : Fact (↑↑μ t < ⊤)
⊢ f =ᶠ[ae (Measure.restrict μ t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    ‖∫ (x : α) in t, f x ∂μ‖ < ENNReal.toReal (↑↑μ t) * C
α : Type u_2
E : Type u_1
F : Type ?u.2692874
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✝ : StrictConvexSpace ℝ E
ht : ↑↑μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂Measure.restrict μ t, ‖f x‖ ≤ C
⊢ f =ᶠ[ae (Measure.restrict μ t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    ‖∫ (x : α) in t, f x ∂μ‖ < ENNReal.toReal (↑↑μ t) * C
haveI := Fact.mk ht.lt_top
α : Type u_2
E : Type u_1
F : Type ?u.2692874
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✝ : StrictConvexSpace ℝ E
ht : ↑↑μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂Measure.restrict μ t, ‖f x‖ ≤ C
this : Fact (↑↑μ t < ⊤)
⊢ f =ᶠ[ae (Measure.restrict μ t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    ‖∫ (x : α) in t, f x ∂μ‖ < ENNReal.toReal (↑↑(Measure.restrict μ t) univ) * C
α : Type u_2
E : Type u_1
F : Type ?u.2692874
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✝ : StrictConvexSpace ℝ E
ht : ↑↑μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂Measure.restrict μ t, ‖f x‖ ≤ C
this : Fact (↑↑μ t < ⊤)
⊢ f =ᶠ[ae (Measure.restrict μ t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    ‖∫ (x : α) in t, f x ∂μ‖ < ENNReal.toReal (↑↑μ t) * C
rw [← restrict_apply_univ]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.2692874
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✝ : StrictConvexSpace ℝ E
ht : ↑↑μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂Measure.restrict μ t, ‖f x‖ ≤ C
this : Fact (↑↑μ t < ⊤)
⊢ f =ᶠ[ae (Measure.restrict μ t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    ‖∫ (x : α) in t, f x ∂μ‖ < ENNReal.toReal (↑↑(Measure.restrict μ t) univ) * C
exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le