case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ Integrable f
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
⊢ Integrable f
obtain ⟨hf_meas_ae, hf⟩ := hf_int
case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ HasFiniteIntegral f
case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ Integrable f
refine' ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, _⟩
case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : (∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm) < ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ') < ⊤
case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ HasFiniteIntegral f
rw [HasFiniteIntegral] at hf ⊢
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : (∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm) < ⊤
⊢ AEMeasurable fun a => ↑‖f a‖₊
case intro
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : (∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm) < ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ') < ⊤
rwa [lintegral_trim_ae hm _] at hf
no goals
α : Type u_1
β : Type ?u.1259200
γ : Type ?u.1259203
δ : Type ?u.1259206
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_2
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : (∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm) < ⊤
⊢ AEMeasurable fun a => ↑‖f a‖₊
exact AEStronglyMeasurable.ennnorm hf_meas_ae