# Functions integrable on a set and at a filter #

We define IntegrableOn f s μ := Integrable f (μ.restrict s) and prove theorems like integrableOn_union : IntegrableOn f (s ∪ t) μ ↔ IntegrableOn f s μ ∧ IntegrableOn f t μ.

Next we define a predicate IntegrableAtFilter (f : α → E) (l : Filter α) (μ : Measure α) saying that f is integrable at some set s ∈ l and prove that a measurable function is integrable at l with respect to μ provided that f is bounded above at l ⊓ ae μ and μ is finite at l.

def StronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (l : ) (μ : ) :

A function f is strongly measurable at a filter l w.r.t. a measure μ if it is ae strongly measurable w.r.t. μ.restrict s for some s ∈ l.

Equations
Instances For
@[simp]
theorem stronglyMeasurableAt_bot {α : Type u_1} {β : Type u_2} [] [] {μ : } {f : αβ} :
theorem StronglyMeasurableAtFilter.eventually {α : Type u_1} {β : Type u_2} [] [] {l : } {f : αβ} {μ : } (h : ) :
∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
theorem StronglyMeasurableAtFilter.filter_mono {α : Type u_1} {β : Type u_2} [] [] {l : } {l' : } {f : αβ} {μ : } (h : ) (h' : l' l) :
theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [] [] {l : } {f : αβ} {μ : } (h : ) :
theorem AeStronglyMeasurable.stronglyMeasurableAtFilter_of_mem {α : Type u_1} {β : Type u_2} [] [] {l : } {f : αβ} {μ : } {s : Set α} (h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hl : s l) :
theorem MeasureTheory.StronglyMeasurable.stronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [] [] {l : } {f : αβ} {μ : } :
theorem MeasureTheory.hasFiniteIntegral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } {C : } (hs : μ s < ) (hf : ∀ᵐ (x : α) ∂μ.restrict s, f x C) :
def MeasureTheory.IntegrableOn {α : Type u_1} {E : Type u_3} [] (f : αE) (s : Set α) (μ : ) :

A function is IntegrableOn a set s if it is almost everywhere strongly measurable on s and if the integral of its pointwise norm over s is less than infinity.

Equations
Instances For
theorem MeasureTheory.IntegrableOn.integrable {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (h : ) :
MeasureTheory.Integrable f (μ.restrict s)
@[simp]
theorem MeasureTheory.integrableOn_empty {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } :
@[simp]
theorem MeasureTheory.integrableOn_univ {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } :
theorem MeasureTheory.integrableOn_zero {α : Type u_1} {E : Type u_3} [] {s : Set α} {μ : } :
MeasureTheory.IntegrableOn (fun (x : α) => 0) s μ
@[simp]
theorem MeasureTheory.integrableOn_const {α : Type u_1} {E : Type u_3} [] {s : Set α} {μ : } {C : E} :
MeasureTheory.IntegrableOn (fun (x : α) => C) s μ C = 0 μ s <
theorem MeasureTheory.IntegrableOn.mono {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } {ν : } (h : ) (hs : s t) (hμ : μ ν) :
theorem MeasureTheory.IntegrableOn.mono_set {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : ) (hst : s t) :
theorem MeasureTheory.IntegrableOn.mono_measure {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } {ν : } (h : ) (hμ : μ ν) :
theorem MeasureTheory.IntegrableOn.mono_set_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : ) (hst : s ≤ᵐ[μ] t) :
theorem MeasureTheory.IntegrableOn.congr_set_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : ) (hst : s =ᵐ[μ] t) :
theorem MeasureTheory.IntegrableOn.congr_fun_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {g : αE} {s : Set α} {μ : } (h : ) (hst : f =ᵐ[μ.restrict s] g) :
theorem MeasureTheory.integrableOn_congr_fun_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {g : αE} {s : Set α} {μ : } (hst : f =ᵐ[μ.restrict s] g) :
theorem MeasureTheory.IntegrableOn.congr_fun {α : Type u_1} {E : Type u_3} [] {f : αE} {g : αE} {s : Set α} {μ : } (h : ) (hst : Set.EqOn f g s) (hs : ) :
theorem MeasureTheory.integrableOn_congr_fun {α : Type u_1} {E : Type u_3} [] {f : αE} {g : αE} {s : Set α} {μ : } (hst : Set.EqOn f g s) (hs : ) :
theorem MeasureTheory.Integrable.integrableOn {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (h : ) :
theorem MeasureTheory.IntegrableOn.restrict {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : ) (hs : ) :
MeasureTheory.IntegrableOn f s (μ.restrict t)
theorem MeasureTheory.IntegrableOn.inter_of_restrict {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : MeasureTheory.IntegrableOn f s (μ.restrict t)) :
theorem MeasureTheory.Integrable.piecewise {α : Type u_1} {E : Type u_3} [] {f : αE} {g : αE} {s : Set α} {μ : } [DecidablePred fun (x : α) => x s] (hs : ) (hf : ) (hg : ) :
MeasureTheory.Integrable (s.piecewise f g) μ
theorem MeasureTheory.IntegrableOn.left_of_union {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : MeasureTheory.IntegrableOn f (s t) μ) :
theorem MeasureTheory.IntegrableOn.right_of_union {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : MeasureTheory.IntegrableOn f (s t) μ) :
theorem MeasureTheory.IntegrableOn.union {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (hs : ) (ht : ) :
@[simp]
theorem MeasureTheory.integrableOn_union {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } :
@[simp]
theorem MeasureTheory.integrableOn_singleton_iff {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {x : α} :
f x = 0 μ {x} <
@[simp]
theorem MeasureTheory.integrableOn_finite_biUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {f : αE} {μ : } {s : Set β} (hs : s.Finite) {t : βSet α} :
MeasureTheory.IntegrableOn f (is, t i) μ is, MeasureTheory.IntegrableOn f (t i) μ
@[simp]
theorem MeasureTheory.integrableOn_finset_iUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {f : αE} {μ : } {s : } {t : βSet α} :
MeasureTheory.IntegrableOn f (is, t i) μ is, MeasureTheory.IntegrableOn f (t i) μ
@[simp]
theorem MeasureTheory.integrableOn_finite_iUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {f : αE} {μ : } [] {t : βSet α} :
MeasureTheory.IntegrableOn f (⋃ (i : β), t i) μ ∀ (i : β), MeasureTheory.IntegrableOn f (t i) μ
theorem MeasureTheory.IntegrableOn.add_measure {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } {ν : } (hμ : ) (hν : ) :
@[simp]
theorem MeasureTheory.integrableOn_add_measure {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } {ν : } :
theorem MeasurableEmbedding.integrableOn_map_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [] [] {e : αβ} (he : ) {f : βE} {μ : } {s : Set β} :
theorem MeasurableEmbedding.integrableOn_iff_comap {α : Type u_1} {β : Type u_2} {E : Type u_3} [] [] {e : αβ} (he : ) {f : βE} {μ : } {s : Set β} (hs : s ) :
theorem MeasureTheory.integrableOn_map_equiv {α : Type u_1} {β : Type u_2} {E : Type u_3} [] [] (e : α ≃ᵐ β) {f : βE} {μ : } {s : Set β} :
theorem MeasureTheory.MeasurePreserving.integrableOn_comp_preimage {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {μ : } [] {e : αβ} {ν : } (h₁ : ) (h₂ : ) {f : βE} {s : Set β} :
theorem MeasureTheory.MeasurePreserving.integrableOn_image {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {μ : } [] {e : αβ} {ν : } (h₁ : ) (h₂ : ) {f : βE} {s : Set α} :
theorem MeasureTheory.integrable_indicator_iff {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (hs : ) :
MeasureTheory.Integrable (s.indicator f) μ
theorem MeasureTheory.IntegrableOn.integrable_indicator {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (h : ) (hs : ) :
MeasureTheory.Integrable (s.indicator f) μ
theorem MeasureTheory.Integrable.indicator {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (h : ) (hs : ) :
MeasureTheory.Integrable (s.indicator f) μ
theorem MeasureTheory.IntegrableOn.indicator {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (h : ) (ht : ) :
MeasureTheory.IntegrableOn (t.indicator f) s μ
theorem MeasureTheory.integrable_indicatorConstLp {α : Type u_1} [] {μ : } {E : Type u_5} {p : ENNReal} {s : Set α} (hs : ) (hμs : μ s ) (c : E) :
theorem MeasureTheory.IntegrableOn.restrict_toMeasurable {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (hf : ) (h's : xs, f x 0) :
μ.restrict = μ.restrict s

If a function is integrable on a set s and nonzero there, then the measurable hull of s is well behaved: the restriction of the measure to toMeasurable μ s coincides with its restriction to s.

theorem MeasureTheory.IntegrableOn.of_ae_diff_eq_zero {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (hf : ) (ht : ) (h't : ∀ᵐ (x : α) ∂μ, x t \ sf x = 0) :

If a function is integrable on a set s, and vanishes on t \ s, then it is integrable on t if t is null-measurable.

theorem MeasureTheory.IntegrableOn.of_forall_diff_eq_zero {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {t : Set α} {μ : } (hf : ) (ht : ) (h't : xt \ s, f x = 0) :

If a function is integrable on a set s, and vanishes on t \ s, then it is integrable on t if t is measurable.

theorem MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (hf : ) (h't : ∀ᵐ (x : α) ∂μ, xsf x = 0) :

If a function is integrable on a set s and vanishes almost everywhere on its complement, then it is integrable.

theorem MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (hf : ) (h't : xs, f x = 0) :

If a function is integrable on a set s and vanishes everywhere on its complement, then it is integrable.

theorem MeasureTheory.integrableOn_iff_integrable_of_support_subset {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (h1s : ) :
theorem MeasureTheory.integrableOn_Lp_of_measure_ne_top {α : Type u_1} [] {μ : } {E : Type u_5} {p : ENNReal} {s : Set α} (f : ()) (hp : 1 p) (hμs : μ s ) :
theorem MeasureTheory.Integrable.lintegral_lt_top {α : Type u_1} [] {μ : } {f : α} (hf : ) :
∫⁻ (x : α), ENNReal.ofReal (f x)μ <
theorem MeasureTheory.IntegrableOn.setLIntegral_lt_top {α : Type u_1} [] {μ : } {f : α} {s : Set α} (hf : ) :
∫⁻ (x : α) in s, ENNReal.ofReal (f x)μ <
@[deprecated MeasureTheory.IntegrableOn.setLIntegral_lt_top]
theorem MeasureTheory.IntegrableOn.set_lintegral_lt_top {α : Type u_1} [] {μ : } {f : α} {s : Set α} (hf : ) :
∫⁻ (x : α) in s, ENNReal.ofReal (f x)μ <

Alias of MeasureTheory.IntegrableOn.setLIntegral_lt_top.

def MeasureTheory.IntegrableAtFilter {α : Type u_1} {E : Type u_3} [] (f : αE) (l : ) (μ : ) :

We say that a function f is integrable at filter l if it is integrable on some set s ∈ l. Equivalently, it is eventually integrable on s in l.smallSets.

Equations
• = sl,
Instances For
theorem MeasurableEmbedding.integrableAtFilter_map_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {μ : } {l : } [] {e : αβ} (he : ) {f : βE} :
theorem MeasurableEmbedding.integrableAtFilter_iff_comap {α : Type u_1} {β : Type u_2} {E : Type u_3} [] {l : } [] {e : αβ} (he : ) {f : βE} {μ : } :
theorem MeasureTheory.Integrable.integrableAtFilter {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } (h : ) (l : ) :
theorem MeasureTheory.IntegrableAtFilter.eventually {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } (h : ) :
∀ᶠ (s : Set α) in l.smallSets,
theorem MeasureTheory.IntegrableAtFilter.add {α : Type u_1} {E : Type u_3} [] {μ : } {l : } {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.IntegrableAtFilter.neg {α : Type u_1} {E : Type u_3} [] {μ : } {l : } {f : αE} (hf : ) :
theorem MeasureTheory.IntegrableAtFilter.sub {α : Type u_1} {E : Type u_3} [] {μ : } {l : } {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.IntegrableAtFilter.smul {α : Type u_1} {E : Type u_3} [] {μ : } {l : } {𝕜 : Type u_5} [] [] {f : αE} (hf : ) (c : 𝕜) :
theorem MeasureTheory.IntegrableAtFilter.norm {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } (hf : ) :
MeasureTheory.IntegrableAtFilter (fun (x : α) => f x) l μ
theorem MeasureTheory.IntegrableAtFilter.filter_mono {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } {l' : } (hl : l l') (hl' : ) :
theorem MeasureTheory.IntegrableAtFilter.inf_of_left {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } {l' : } (hl : ) :
theorem MeasureTheory.IntegrableAtFilter.inf_of_right {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } {l' : } (hl : ) :
@[simp]
theorem MeasureTheory.IntegrableAtFilter.inf_ae_iff {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } :
theorem MeasureTheory.IntegrableAtFilter.of_inf_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } :

Alias of the forward direction of MeasureTheory.IntegrableAtFilter.inf_ae_iff.

@[simp]
theorem MeasureTheory.integrableAtFilter_top {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } :
theorem MeasureTheory.IntegrableAtFilter.sup_iff {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } {l' : } :
theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } [l.IsMeasurablyGenerated] (hfm : ) (hμ : μ.FiniteAtFilter l) (hf : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)) :

If μ is a measure finite at filter l and f is a function such that its norm is bounded above at l, then f is integrable at l.

theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } [l.IsMeasurablyGenerated] (hfm : ) (hμ : μ.FiniteAtFilter l) {b : E} (hf : Filter.Tendsto f () (nhds b)) :
theorem Filter.Tendsto.integrableAtFilter_ae {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } [l.IsMeasurablyGenerated] (hfm : ) (hμ : μ.FiniteAtFilter l) {b : E} (hf : Filter.Tendsto f () (nhds b)) :

Alias of MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae.

theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } [l.IsMeasurablyGenerated] (hfm : ) (hμ : μ.FiniteAtFilter l) {b : E} (hf : Filter.Tendsto f l (nhds b)) :
theorem Filter.Tendsto.integrableAtFilter {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } [l.IsMeasurablyGenerated] (hfm : ) (hμ : μ.FiniteAtFilter l) {b : E} (hf : Filter.Tendsto f l (nhds b)) :

Alias of MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto.

theorem MeasureTheory.Measure.integrableOn_of_bounded {α : Type u_1} {E : Type u_3} [] {f : αE} {s : Set α} {μ : } (s_finite : μ s ) (f_mble : ) {M : } (f_bdd : ∀ᵐ (a : α) ∂μ.restrict s, f a M) :
theorem MeasureTheory.integrable_add_of_disjoint {α : Type u_1} {E : Type u_3} [] {μ : } {f : αE} {g : αE} (h : ) (hf : ) (hg : ) :
theorem MeasureTheory.IntegrableAtFilter.eq_zero_of_tendsto {α : Type u_1} {E : Type u_3} [] {f : αE} {μ : } {l : } (h : ) (h' : sl, μ s = ) {a : E} (hf : Filter.Tendsto f l (nhds a)) :
a = 0

If a function converges along a filter to a limit a, is integrable along this filter, and all elements of the filter have infinite measure, then the limit has to vanish.

theorem ContinuousOn.aemeasurable {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {s : Set α} {μ : } (hf : ) (hs : ) :
AEMeasurable f (μ.restrict s)

A function which is continuous on a set s is almost everywhere measurable with respect to μ.restrict s.

theorem ContinuousOn.aestronglyMeasurable_of_isSeparable {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} {μ : } (hf : ) (hs : ) (h's : ) :

A function which is continuous on a separable set s is almost everywhere strongly measurable with respect to μ.restrict s.

theorem ContinuousOn.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [] [] [] [h : ] {f : αβ} {s : Set α} {μ : } (hf : ) (hs : ) :

A function which is continuous on a set s is almost everywhere strongly measurable with respect to μ.restrict s when either the source space or the target space is second-countable.

theorem ContinuousOn.aestronglyMeasurable_of_isCompact {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} {μ : } (hf : ) (hs : ) (h's : ) :

A function which is continuous on a compact set s is almost everywhere strongly measurable with respect to μ.restrict s.

theorem ContinuousOn.integrableAt_nhdsWithin_of_isSeparable {α : Type u_1} {E : Type u_3} [] [] {μ : } {a : α} {t : Set α} {f : αE} (hft : ) (ht : ) (h't : ) (ha : a t) :
theorem ContinuousOn.integrableAt_nhdsWithin {α : Type u_1} {E : Type u_3} [] [] {μ : } {a : α} {t : Set α} {f : αE} (hft : ) (ht : ) (ha : a t) :
theorem Continuous.integrableAt_nhds {α : Type u_1} {E : Type u_3} [] [] {μ : } {f : αE} (hf : ) (a : α) :
theorem ContinuousOn.stronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} {μ : } (hs : ) (hf : ) (x : α) :
x s

If a function is continuous on an open set s, then it is strongly measurable at the filter 𝓝 x for all x ∈ s if either the source space or the target space is second-countable.

theorem ContinuousAt.stronglyMeasurableAtFilter {α : Type u_1} {E : Type u_3} [] [] {f : αE} {s : Set α} {μ : } (hs : ) (hf : xs, ) (x : α) :
x s
theorem Continuous.stronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) (μ : ) (l : ) :
theorem ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin {α : Type u_5} {β : Type u_6} [] [] [] {f : αβ} {s : Set α} {μ : } (hf : ) (hs : ) (x : α) :

If a function is continuous on a measurable set s, then it is measurable at the filter 𝓝[s] x for all x.

The primed lemmas take explicit arguments about the measure being finite at the endpoint, while the unprimed ones use [NoAtoms μ].

theorem integrableOn_Icc_iff_integrableOn_Ioc' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} (ha : μ {a} ) :
theorem integrableOn_Icc_iff_integrableOn_Ico' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} (hb : μ {b} ) :
theorem integrableOn_Ico_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} (ha : μ {a} ) :
theorem integrableOn_Ioc_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} (hb : μ {b} ) :
theorem integrableOn_Icc_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} (ha : μ {a} ) (hb : μ {b} ) :
theorem integrableOn_Ici_iff_integrableOn_Ioi' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {b : α} (hb : μ {b} ) :
theorem integrableOn_Iic_iff_integrableOn_Iio' {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {b : α} (hb : μ {b} ) :
theorem integrableOn_Icc_iff_integrableOn_Ioc {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} :
theorem integrableOn_Icc_iff_integrableOn_Ico {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} :
theorem integrableOn_Ico_iff_integrableOn_Ioo {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} :
theorem integrableOn_Ioc_iff_integrableOn_Ioo {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} :
theorem integrableOn_Icc_iff_integrableOn_Ioo {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {a : α} {b : α} :
theorem integrableOn_Ici_iff_integrableOn_Ioi {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {b : α} :
theorem integrableOn_Iic_iff_integrableOn_Iio {α : Type u_1} {E : Type u_3} [] [] {f : αE} {μ : } {b : α} :