α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
⊢ ↑‖c‖₊ ≤ snormEssSup (Set.indicator s fun x => c) μ
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
⊢ snormEssSup (Set.indicator s fun x => c) μ = ↑‖c‖₊
refine' le_antisymm (snormEssSup_indicator_const_le s c) _
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
⊢ False
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
⊢ ↑‖c‖₊ ≤ snormEssSup (Set.indicator s fun x => c) μ
by_contra' h
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ¬↑‖Set.indicator s (fun x => c) a‖₊ < ↑‖c‖₊} = 0
⊢ False
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
⊢ False
have h' := ae_iff.mp (ae_lt_of_essSup_lt h)
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊} = 0
⊢ False
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ¬↑‖Set.indicator s (fun x => c) a‖₊ < ↑‖c‖₊} = 0
⊢ False
push_neg  at h'
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊} = 0
x : α
hx_mem : x ∈ s
⊢ x ∈ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊}
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊} = 0
⊢ False
refine' hμs (measure_mono_null (fun x hx_mem => _) h')
no goals
α : Type u_1
E : Type ?u.635109
F : Type ?u.635112
G : Type u_2
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 μ
s : Set α
c : G
hμs : ↑↑μ s ≠ 0
h : snormEssSup (Set.indicator s fun x => c) μ < ↑‖c‖₊
h' : ↑↑μ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊} = 0
x : α
hx_mem : x ∈ s
⊢ x ∈ {a | ↑‖c‖₊ ≤ ↑‖Set.indicator s (fun x => c) a‖₊}
rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem]