α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ sInf {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (Measure.ae (Measure.trim ν hm)) = limsup f (Measure.ae ν)
simp_rw [limsup_eq]
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
h_set_eq : {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
⊢ sInf {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}

case h_set_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ sInf {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
suffices h_set_eq : { a : ℝ≥0∞ | ∀ᵐ n ∂ν.trim hm, f n ≤ a } = { a : ℝ≥0∞ | ∀ᵐ n ∂ν, f n ≤ a }
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ a ∈ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
case h_set_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
ext1 a
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
⊢ a ∈ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}

case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ a ∈ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
suffices h_meas_eq : ν { x | ¬f x ≤ a } = ν.trim hm { x | ¬f x ≤ a }
case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet {x | ¬f x ≤ a}
case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
refine' (trim_measurableSet_eq hm _).symm
case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Measurable fun x => a
case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ MeasurableSet {x | ¬f x ≤ a}
refine' @MeasurableSet.compl _ _ m (@measurableSet_le ℝ≥0∞ _ _ _ _ m _ _ _ _ _ hf _)
no goals
case h_meas_eq
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
⊢ Measurable fun x => a
exact @measurable_const _ _ _ m _
no goals
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
h_set_eq : {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
⊢ sInf {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
rw [h_set_eq]
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
⊢ (∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a) ↔ ↑↑(Measure.trim ν hm) {a_1 | ¬f a_1 ≤ a} = 0
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
⊢ a ∈ {a | ∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂ν, f n ≤ a}
simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]
no goals
case h_set_eq.h
α : Type u_1
E : Type ?u.3170438
F : Type ?u.3170441
G : Type ?u.3170444
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : ↑↑ν {x | ¬f x ≤ a} = ↑↑(Measure.trim ν hm) {x | ¬f x ≤ a}
⊢ (∀ᵐ (n : α) ∂Measure.trim ν hm, f n ≤ a) ↔ ↑↑(Measure.trim ν hm) {a_1 | ¬f a_1 ≤ a} = 0
rfl