Theorem: integrableOn_Ici_iff_integrableAtFilter_atTop (PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean)

State before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ IntegrableOn f (Ici a) μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
Tactic:
refine ⟨fun h ↦ ⟨⟨Ici a, Ici_mem_atTop a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩
State after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
⊢ IntegrableOn f (Ici a) μ

State before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
⊢ IntegrableOn f (Ici a) μ
Tactic:
haveI : Nonempty X := Nonempty.intro a
State after:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
⊢ IntegrableOn f (Ici a) μ

State before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
⊢ IntegrableOn f (Ici a) μ
Tactic:
obtain ⟨a', ha'⟩ := mem_atTop_sets.mp hsl
State after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Ici a) μ

State before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Ici a) μ
Tactic:
refine (integrableOn_union.mpr ⟨?_, hs.mono ha' le_rfl⟩).mono Ici_subset_Icc_union_Ici le_rfl
State after:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Icc a a') μ

State before:
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Icc a a') μ
Tactic:
exact h.integrableOn_compact_subset Icc_subset_Ici_self isCompact_Icc
State after:
no goals