α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ Memℒp (f + g) p ↔ Memℒp f p ∧ Memℒp g p
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Memℒp (f + g) p ↔ Memℒp f p ∧ Memℒp g p
borelize E
case refine'_1
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp f p

case refine'_2
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp g p
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ Memℒp (f + g) p ↔ Memℒp f p ∧ Memℒp g p
refine' ⟨fun hfg => ⟨_, _⟩, fun h => h.1.add h.2⟩
case refine'_1
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp (Set.indicator (support f) (f + g)) p
case refine'_1
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp f p
rw [← Set.indicator_add_eq_left h]
no goals
case refine'_1
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp (Set.indicator (support f) (f + g)) p
exact hfg.indicator (measurableSet_support hf.measurable)
case refine'_2
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp (Set.indicator (support g) (f + g)) p
case refine'_2
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp g p
rw [← Set.indicator_add_eq_right h]
no goals
case refine'_2
α : Type u_1
E : Type u_2
F : Type ?u.704975
G : Type ?u.704978
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : Memℒp (f + g) p
⊢ Memℒp (Set.indicator (support g) (f + g)) p
exact hfg.indicator (measurableSet_support hg.measurable)