α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
⊢ snormEssSup (Set.indicator s f) μ = snormEssSup f (Measure.restrict μ s)
simp_rw [snormEssSup, nnnorm_indicator_eq_indicator_nnnorm, ENNReal.coe_indicator]
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)

case neg
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)
by_cases hs_null : μ s = 0
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
x : α
⊢ OfNat.ofNat 0 x ≤ ↑‖f x‖₊
case neg
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)
rw [essSup_indicator_eq_essSup_restrict (eventually_of_forall fun x => ?_) hs hs_null]
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
x : α
⊢ 0 ≤ ↑‖f x‖₊
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
x : α
⊢ OfNat.ofNat 0 x ≤ ↑‖f x‖₊
rw [Pi.zero_apply]
no goals
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ¬↑↑μ s = 0
x : α
⊢ 0 ≤ ↑‖f x‖₊
exact zero_le _
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) 0
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) (Measure.restrict μ s)
rw [Measure.restrict_zero_set hs_null]
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ essSup (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) μ = essSup (fun x => ↑‖f x‖₊) 0
simp only [essSup_measure_zero, ENNReal.essSup_eq_zero_iff, ENNReal.bot_eq_zero]
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) =ᵐ[μ] 0
have hs_empty : s =ᵐ[μ] (∅ : Set α) := by rw [ae_eq_set]; simpa using hs_null
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (Set.indicator ∅ fun x => ↑‖f x‖₊) =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (fun x => Set.indicator s (fun x => ↑‖f x‖₊) x) =ᵐ[μ] 0
refine' (indicator_ae_eq_of_ae_eq_set hs_empty).trans _
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (fun x => 0) =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (Set.indicator ∅ fun x => ↑‖f x‖₊) =ᵐ[μ] 0
rw [Set.indicator_empty]
no goals
case pos
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
hs_empty : s =ᵐ[μ] ∅
⊢ (fun x => 0) =ᵐ[μ] 0
rfl
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ ↑↑μ (s \ ∅) = 0 ∧ ↑↑μ (∅ \ s) = 0
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ s =ᵐ[μ] ∅
rw [ae_eq_set]
no goals
α : Type u_1
E : Type ?u.655000
F : Type u_2
G : Type ?u.655006
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✝ μ
f : α → F
hs : MeasurableSet s
hs_null : ↑↑μ s = 0
⊢ ↑↑μ (s \ ∅) = 0 ∧ ↑↑μ (∅ \ s) = 0
simpa using hs_null