α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
⊢ Memℒp (fun x => c) p
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
⊢ Memℒp (Set.indicator s fun x => c) p
rw [memℒp_indicator_iff_restrict hs]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : p = 0
⊢ Memℒp (fun x => c) p

case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
⊢ Memℒp (fun x => c) p
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
⊢ Memℒp (fun x => c) p
by_cases hp_zero : p = 0
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (fun x => c) p

case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ Memℒp (fun x => c) p
case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
⊢ Memℒp (fun x => c) p
by_cases hp_top : p = ∞
case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ c = 0 ∨ ↑↑μ s < ⊤
case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ Memℒp (fun x => c) p
rw [memℒp_const_iff hp_zero hp_top, Measure.restrict_apply_univ]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ c = 0 ∨ ↑↑μ s < ⊤
cases hμsc with
| inl hμsc => exact Or.inl hμsc
| inr hμsc => exact Or.inr hμsc.lt_top
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : p = 0
⊢ Memℒp (fun x => c) 0
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : p = 0
⊢ Memℒp (fun x => c) p
rw [hp_zero]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : p = 0
⊢ Memℒp (fun x => c) 0
exact memℒp_zero_iff_aestronglyMeasurable.mpr aestronglyMeasurable_const
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (fun x => c) ⊤
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (fun x => c) p
rw [hp_top]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ ↑↑μ s ≠ ⊤
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (fun x => c) ⊤
exact
  memℒp_top_of_bound aestronglyMeasurable_const ‖c‖ (eventually_of_forall fun _ => le_rfl)
no goals
case neg.inl
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
hμsc : c = 0
⊢ c = 0 ∨ ↑↑μ s < ⊤
exact Or.inl hμsc
no goals
case neg.inr
α : Type u_1
E : Type u_2
F : Type ?u.667132
G : Type ?u.667135
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs✝ : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
hμsc : ↑↑μ s ≠ ⊤
⊢ c = 0 ∨ ↑↑μ s < ⊤
exact Or.inr hμsc.lt_top