case refine'_1
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable f

case refine'_2
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable g
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) ↔ Integrable f ∧ Integrable g
refine' ⟨fun hfg => ⟨_, _⟩, fun h => h.1.add h.2⟩
case refine'_1
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support f) (f + g))
case refine'_1
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable f
rw [← indicator_add_eq_left h]
no goals
case refine'_1
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support f) (f + g))
exact hfg.indicator hf.measurableSet_support
case refine'_2
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support g) (f + g))
case refine'_2
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable g
rw [← indicator_add_eq_right h]
no goals
case refine'_2
α : Type u_1
β : Type ?u.1665526
E : Type u_2
F : Type ?u.1665532
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support g) (f + g))
exact hfg.indicator hg.measurableSet_support