X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
⊢ IntegrableAtFilter f (𝓝 x)
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
⊢ LocallyIntegrableOn f s ↔ LocallyIntegrable f
refine' ⟨fun hf x => _, locallyIntegrableOn_of_locallyIntegrable_restrict⟩
case pos
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)

case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
⊢ IntegrableAtFilter f (𝓝 x)
by_cases h : x ∈ s
case pos.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
⊢ IntegrableAtFilter f (𝓝 x)
case pos
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)
obtain ⟨t, ht_nhds, ht_int⟩ := hf x h
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝 x)
case pos.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
⊢ IntegrableAtFilter f (𝓝 x)
obtain ⟨u, hu_o, hu_x, hu_sub⟩ := mem_nhdsWithin.mp ht_nhds
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableOn f u
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝 x)
refine' ⟨u, hu_o.mem_nhds hu_x, _⟩
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableOn f u
rw [IntegrableOn, restrict_restrict hu_o.measurableSet]
no goals
case pos.intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t
u : Set X
hu_o : IsOpen u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f
exact ht_int.mono_set hu_sub
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed s
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)
rw [← isOpen_compl_iff] at hs
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableOn f (sᶜ)
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableAtFilter f (𝓝 x)
refine' ⟨sᶜ, hs.mem_nhds h, _⟩
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableOn f ∅

case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ MeasurableSet (sᶜ)
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableOn f (sᶜ)
rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]
no goals
case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ IntegrableOn f ∅

case neg
X : Type u_1
Y : Type ?u.123754
E : Type u_2
R : Type ?u.123760
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen (sᶜ)
hf : LocallyIntegrableOn f s
x : X
h : ¬x ∈ s
⊢ MeasurableSet (sᶜ)
exacts [integrableOn_empty, hs.measurableSet]