α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑μ s)
apply norm_set_integral_le_of_norm_le_const_ae hs
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
have A : ∀ᵐ x : α ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C := by
  filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
  rw [← h2 h3]
  exact h1 h3
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
have B : MeasurableSet {x | ‖(hfm.mk f) x‖ ≤ C} :=
  hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
a✝¹ : α
h1 : f a✝¹ = AEStronglyMeasurable.mk f hfm a✝¹
a✝ : ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C
⊢ ‖f a✝¹‖ ≤ C
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
no goals
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
A : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
a✝¹ : α
h1 : f a✝¹ = AEStronglyMeasurable.mk f hfm a✝¹
a✝ : ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C
⊢ ‖f a✝¹‖ ≤ C
rwa [h1]
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
a✝ : α
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖AEStronglyMeasurable.mk f hfm a✝‖ ≤ C
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
a✝ : α
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
a✝ : α
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖AEStronglyMeasurable.mk f hfm a✝‖ ≤ C
rw [← h2 h3]
no goals
case h
α : Type u_1
β : Type ?u.254346
E : Type u_2
F : Type ?u.254352
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (Measure.restrict μ s)
a✝ : α
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C
exact h1 h3