α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
⊢ IntegrableAtFilter f (l ⊓ Measure.ae μ) → IntegrableAtFilter f l
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
⊢ IntegrableAtFilter f (l ⊓ Measure.ae μ) ↔ IntegrableAtFilter f l
refine' ⟨_, fun h => h.filter_mono inf_le_left⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableAtFilter f l
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
⊢ IntegrableAtFilter f (l ⊓ Measure.ae μ) → IntegrableAtFilter f l
rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableOn f t
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableAtFilter f l
refine' ⟨t, ht, _⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑(Measure.restrict μ t) v ≤ ↑↑(Measure.restrict μ (t ∩ u)) v
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableOn f t
refine' hf.integrable.mono_measure fun v hv => _
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑μ (v ∩ t) ≤ ↑↑μ (v ∩ (t ∩ u))
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑(Measure.restrict μ t) v ≤ ↑↑(Measure.restrict μ (t ∩ u)) v
simp only [Measure.restrict_apply hv]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
x : α
hx : x ∈ u
⊢ x ∈ {x | (fun x => (v ∩ t) x ≤ (v ∩ (t ∩ u)) x) x}
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑μ (v ∩ t) ≤ ↑↑μ (v ∩ (t ∩ u))
refine' measure_mono_ae (mem_of_superset hu fun x hx => _)
no goals
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1660656
E : Type u_2
F : Type ?u.1660662
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
x : α
hx : x ∈ u
⊢ x ∈ {x | (fun x => (v ∩ t) x ≤ (v ∩ (t ∩ u)) x) x}
exact fun ⟨hv, ht⟩ => ⟨hv, ⟨ht, hx⟩⟩