α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂Measure.trim ν hm) ^ (1 / q) = (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂ν) ^ (1 / q)
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ snorm' f q (Measure.trim ν hm) = snorm' f q ν
simp_rw [snorm']
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂Measure.trim ν hm) = ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂ν
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂Measure.trim ν hm) ^ (1 / q) = (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂ν) ^ (1 / q)
congr 1
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ↑‖f a‖₊ ^ q
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂Measure.trim ν hm) = ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂ν
refine' lintegral_trim hm _
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖₊
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ↑‖f a‖₊ ^ q
refine' @Measurable.pow_const _ _ _ _ _ _ _ m _ (@Measurable.coe_nnreal_ennreal _ m _ _) q
case e_a.hf
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun a => ‖f a‖₊
case e_a
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖₊
apply @StronglyMeasurable.measurable
no goals
case e_a.hf
α : Type u_1
E : Type u_2
F : Type ?u.3169381
G : Type ?u.3169384
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun a => ‖f a‖₊
exact @StronglyMeasurable.nnnorm α m _ _ _ hf