α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ Memℒp (↑↑f) 1
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ IntegrableOn (↑↑f) s
refine' memℒp_one_iff_integrable.mp _
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
⊢ Memℒp (↑↑f) 1
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ Memℒp (↑↑f) 1
have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
  simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
hμ_finite : IsFiniteMeasure (Measure.restrict μ s)
⊢ Memℒp (↑↑f) 1
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
⊢ Memℒp (↑↑f) 1
haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
no goals
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
hμ_finite : IsFiniteMeasure (Measure.restrict μ s)
⊢ Memℒp (↑↑f) 1
exact ((Lp.memℒp _).restrict s).memℒp_of_exponent_le hp
no goals
α : Type u_2
β : Type ?u.1655667
E✝ : Type ?u.1655670
F : Type ?u.1655673
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_1
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ ↑↑(Measure.restrict μ s) univ < ⊤
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]