α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
ε : ℝ
hε : 0 < ε
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
have hℒp := hf
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
obtain ⟨⟨f', hf', heq⟩, _⟩ := hf
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ, hδpos, hδ⟩ := (hℒp.ae_eq heq).snorm_indicator_le_of_meas μ hp_one hp_top hf' hε
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
refine' ⟨δ, hδpos, fun s hs hμs => _⟩
case h.e'_3
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ = snorm (Set.indicator s f') p μ
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
convert hδ s hs hμs using 1
case h.e'_3
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm f p (Measure.restrict μ s) = snorm f' p (Measure.restrict μ s)
case h.e'_3
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ = snorm (Set.indicator s f') p μ
rw [snorm_indicator_eq_snorm_restrict hs, snorm_indicator_eq_snorm_restrict hs]
no goals
case h.e'_3
α : Type u_2
β : Type u_1
ι : Type ?u.150616
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
hℒp : Memℒp f p
right✝ : snorm f p μ < ⊤
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm f p (Measure.restrict μ s) = snorm f' p (Measure.restrict μ s)
refine' snorm_congr_ae heq.restrict