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}
[MeasurableSpace α]
[TopologicalSpace β]
(f : α → β)
(l : Filter α)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
- StronglyMeasurableAtFilter f l μ = ∃ s ∈ l, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
Instances For
@[simp]
theorem
stronglyMeasurableAt_bot
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
:
theorem
StronglyMeasurableAtFilter.eventually
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : StronglyMeasurableAtFilter f l μ)
:
∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
theorem
StronglyMeasurableAtFilter.filter_mono
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l l' : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : StronglyMeasurableAtFilter f l μ)
(h' : l' ≤ l)
:
StronglyMeasurableAtFilter f l' μ
theorem
MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
AeStronglyMeasurable.stronglyMeasurableAtFilter_of_mem
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
(hl : s ∈ l)
:
theorem
MeasureTheory.StronglyMeasurable.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.StronglyMeasurable f)
:
theorem
MeasureTheory.hasFiniteIntegral_restrict_of_bounded
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
{C : ℝ}
(hs : μ s < ⊤)
(hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C)
:
MeasureTheory.HasFiniteIntegral f (μ.restrict s)
def
MeasureTheory.IntegrableOn
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(f : α → E)
(s : Set α)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
- MeasureTheory.IntegrableOn f s μ = MeasureTheory.Integrable f (μ.restrict s)
Instances For
theorem
MeasureTheory.IntegrableOn.integrable
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
:
MeasureTheory.Integrable f (μ.restrict s)
@[simp]
theorem
MeasureTheory.integrableOn_empty
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.integrableOn_univ
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn f Set.univ μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrableOn_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{s : Set α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn (fun (x : α) => 0) s μ
@[simp]
theorem
MeasureTheory.integrableOn_const
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{s : Set α}
{μ : MeasureTheory.Measure α}
{C : E}
:
theorem
MeasureTheory.IntegrableOn.mono
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ ν : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t ν)
(hs : s ⊆ t)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.IntegrableOn.mono_set
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t μ)
(hst : s ⊆ t)
:
theorem
MeasureTheory.IntegrableOn.mono_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ ν : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s ν)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.IntegrableOn.mono_set_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t μ)
(hst : s ≤ᵐ[μ] t)
:
theorem
MeasureTheory.IntegrableOn.congr_set_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t μ)
(hst : s =ᵐ[μ] t)
:
theorem
MeasureTheory.IntegrableOn.congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
(hst : f =ᵐ[μ.restrict s] g)
:
theorem
MeasureTheory.integrableOn_congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hst : f =ᵐ[μ.restrict s] g)
:
MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ
theorem
MeasureTheory.IntegrableOn.congr_fun
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
(hst : Set.EqOn f g s)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.integrableOn_congr_fun
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hst : Set.EqOn f g s)
(hs : MeasurableSet s)
:
MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ
theorem
MeasureTheory.Integrable.integrableOn
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.IntegrableOn.restrict
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
(hs : MeasurableSet s)
:
MeasureTheory.IntegrableOn f s (μ.restrict t)
theorem
MeasureTheory.IntegrableOn.inter_of_restrict
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s (μ.restrict t))
:
MeasureTheory.IntegrableOn f (s ∩ t) μ
theorem
MeasureTheory.Integrable.piecewise
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g sᶜ μ)
:
MeasureTheory.Integrable (s.piecewise f g) μ
theorem
MeasureTheory.IntegrableOn.left_of_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f (s ∪ t) μ)
:
theorem
MeasureTheory.IntegrableOn.right_of_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f (s ∪ t) μ)
:
theorem
MeasureTheory.IntegrableOn.union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(hs : MeasureTheory.IntegrableOn f s μ)
(ht : MeasureTheory.IntegrableOn f t μ)
:
MeasureTheory.IntegrableOn f (s ∪ t) μ
@[simp]
theorem
MeasureTheory.integrableOn_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn f (s ∪ t) μ ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f t μ
@[simp]
theorem
MeasureTheory.integrableOn_singleton_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{x : α}
[MeasurableSingletonClass α]
:
@[simp]
theorem
MeasureTheory.integrableOn_finite_biUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
(hs : s.Finite)
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
@[simp]
theorem
MeasureTheory.integrableOn_finset_iUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{s : Finset β}
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
@[simp]
theorem
MeasureTheory.integrableOn_finite_iUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
[Finite β]
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ (i : β), t i) μ ↔ ∀ (i : β), MeasureTheory.IntegrableOn f (t i) μ
theorem
MeasureTheory.IntegrableOn.finset
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSingletonClass α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{s : Finset α}
{f : α → E}
:
MeasureTheory.IntegrableOn f (↑s) μ
theorem
MeasureTheory.IntegrableOn.of_finite
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSingletonClass α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set α}
(hs : s.Finite)
{f : α → E}
:
theorem
MeasureTheory.IntegrableOn.add_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ ν : MeasureTheory.Measure α}
(hμ : MeasureTheory.IntegrableOn f s μ)
(hν : MeasureTheory.IntegrableOn f s ν)
:
MeasureTheory.IntegrableOn f s (μ + ν)
@[simp]
theorem
MeasureTheory.integrableOn_add_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ ν : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn f s (μ + ν) ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f s ν
theorem
MeasurableEmbedding.integrableOn_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
:
MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ
theorem
MeasurableEmbedding.integrableOn_iff_comap
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure β}
{s : Set β}
(hs : s ⊆ Set.range e)
:
MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) (MeasureTheory.Measure.comap e μ)
theorem
MeasureTheory.integrableOn_map_equiv
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{f : β → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
:
MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ
theorem
MeasureTheory.MeasurePreserving.integrableOn_comp_preimage
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
[MeasurableSpace β]
{e : α → β}
{ν : MeasureTheory.Measure β}
(h₁ : MeasureTheory.MeasurePreserving e μ ν)
(h₂ : MeasurableEmbedding e)
{f : β → E}
{s : Set β}
:
MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ ↔ MeasureTheory.IntegrableOn f s ν
theorem
MeasureTheory.MeasurePreserving.integrableOn_image
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
[MeasurableSpace β]
{e : α → β}
{ν : MeasureTheory.Measure β}
(h₁ : MeasureTheory.MeasurePreserving e μ ν)
(h₂ : MeasurableEmbedding e)
{f : β → E}
{s : Set α}
:
MeasureTheory.IntegrableOn f (e '' s) ν ↔ MeasureTheory.IntegrableOn (f ∘ e) s μ
theorem
MeasureTheory.integrable_indicator_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (s.indicator f) μ ↔ MeasureTheory.IntegrableOn f s μ
theorem
MeasureTheory.IntegrableOn.integrable_indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (s.indicator f) μ
theorem
MeasureTheory.Integrable.indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f μ)
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (s.indicator f) μ
theorem
MeasureTheory.IntegrableOn.indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s μ)
(ht : MeasurableSet t)
:
MeasureTheory.IntegrableOn (t.indicator f) s μ
theorem
MeasureTheory.integrable_indicatorConstLp
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{p : ENNReal}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : E)
:
MeasureTheory.Integrable (↑↑(MeasureTheory.indicatorConstLp p hs hμs c)) μ
theorem
MeasureTheory.IntegrableOn.restrict_toMeasurable
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s μ)
(h's : ∀ x ∈ s, f x ≠ 0)
:
μ.restrict (MeasureTheory.toMeasurable μ s) = μ.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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s μ)
(ht : MeasureTheory.NullMeasurableSet t μ)
(h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ 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 null-measurable.
theorem
MeasureTheory.IntegrableOn.of_forall_diff_eq_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s μ)
(ht : MeasurableSet t)
(h't : ∀ x ∈ t \ 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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s μ)
(h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f 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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s μ)
(h't : ∀ x ∉ s, 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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h1s : Function.support f ⊆ s)
:
theorem
MeasureTheory.integrableOn_Lp_of_measure_ne_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{p : ENNReal}
{s : Set α}
(f : ↥(MeasureTheory.Lp E p μ))
(hp : 1 ≤ p)
(hμs : μ s ≠ ⊤)
:
MeasureTheory.IntegrableOn (↑↑f) s μ
theorem
MeasureTheory.Integrable.lintegral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ⊤
theorem
MeasureTheory.IntegrableOn.setLIntegral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{s : Set α}
(hf : MeasureTheory.IntegrableOn f s μ)
:
∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ⊤
@[deprecated MeasureTheory.IntegrableOn.setLIntegral_lt_top]
theorem
MeasureTheory.IntegrableOn.set_lintegral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{s : Set α}
(hf : MeasureTheory.IntegrableOn f s μ)
:
∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ⊤
def
MeasureTheory.IntegrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(f : α → E)
(l : Filter α)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
- MeasureTheory.IntegrableAtFilter f l μ = ∃ s ∈ l, MeasureTheory.IntegrableOn f s μ
Instances For
theorem
MeasurableEmbedding.integrableAtFilter_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
:
MeasureTheory.IntegrableAtFilter f (Filter.map e l) (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l μ
theorem
MeasurableEmbedding.integrableAtFilter_iff_comap
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{l : Filter α}
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure β}
:
MeasureTheory.IntegrableAtFilter f (Filter.map e l) μ ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l (MeasureTheory.Measure.comap e μ)
theorem
MeasureTheory.Integrable.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f μ)
(l : Filter α)
:
theorem
MeasureTheory.IntegrableAtFilter.eventually
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
(h : MeasureTheory.IntegrableAtFilter f l μ)
:
∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.IntegrableOn f s μ
theorem
MeasureTheory.IntegrableAtFilter.add
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f g : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l μ)
(hg : MeasureTheory.IntegrableAtFilter g l μ)
:
MeasureTheory.IntegrableAtFilter (f + g) l μ
theorem
MeasureTheory.IntegrableAtFilter.neg
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l μ)
:
theorem
MeasureTheory.IntegrableAtFilter.sub
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f g : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l μ)
(hg : MeasureTheory.IntegrableAtFilter g l μ)
:
MeasureTheory.IntegrableAtFilter (f - g) l μ
theorem
MeasureTheory.IntegrableAtFilter.smul
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{𝕜 : Type u_5}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l μ)
(c : 𝕜)
:
MeasureTheory.IntegrableAtFilter (c • f) l μ
theorem
MeasureTheory.IntegrableAtFilter.norm
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
(hf : MeasureTheory.IntegrableAtFilter f l μ)
:
MeasureTheory.IntegrableAtFilter (fun (x : α) => ‖f x‖) l μ
theorem
MeasureTheory.IntegrableAtFilter.filter_mono
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l l' : Filter α}
(hl : l ≤ l')
(hl' : MeasureTheory.IntegrableAtFilter f l' μ)
:
theorem
MeasureTheory.IntegrableAtFilter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l l' : Filter α}
(hl : MeasureTheory.IntegrableAtFilter f l μ)
:
MeasureTheory.IntegrableAtFilter f (l ⊓ l') μ
theorem
MeasureTheory.IntegrableAtFilter.inf_of_right
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l l' : Filter α}
(hl : MeasureTheory.IntegrableAtFilter f l μ)
:
MeasureTheory.IntegrableAtFilter f (l' ⊓ l) μ
@[simp]
theorem
MeasureTheory.IntegrableAtFilter.inf_ae_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
:
theorem
MeasureTheory.IntegrableAtFilter.of_inf_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
:
MeasureTheory.IntegrableAtFilter f (l ⊓ MeasureTheory.ae μ) μ → MeasureTheory.IntegrableAtFilter f l μ
Alias of the forward direction of MeasureTheory.IntegrableAtFilter.inf_ae_iff.
@[simp]
theorem
MeasureTheory.integrableAtFilter_top
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.IntegrableAtFilter.sup_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l l' : Filter α}
:
MeasureTheory.IntegrableAtFilter f (l ⊔ l') μ ↔ MeasureTheory.IntegrableAtFilter f l μ ∧ MeasureTheory.IntegrableAtFilter f l' μ
theorem
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[l.IsMeasurablyGenerated]
(hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l)
(hf : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[l.IsMeasurablyGenerated]
(hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l)
{b : E}
(hf : Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b))
:
theorem
Filter.Tendsto.integrableAtFilter_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[l.IsMeasurablyGenerated]
(hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l)
{b : E}
(hf : Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[l.IsMeasurablyGenerated]
(hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l)
{b : E}
(hf : Filter.Tendsto f l (nhds b))
:
theorem
Filter.Tendsto.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[l.IsMeasurablyGenerated]
(hfm : StronglyMeasurableAtFilter f l μ)
(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}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(s_finite : μ s ≠ ⊤)
(f_mble : MeasureTheory.AEStronglyMeasurable f μ)
{M : ℝ}
(f_bdd : ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ M)
:
theorem
MeasureTheory.integrable_add_of_disjoint
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
(h : Disjoint (Function.support f) (Function.support g))
(hf : MeasureTheory.StronglyMeasurable f)
(hg : MeasureTheory.StronglyMeasurable g)
:
MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
theorem
MeasureTheory.IntegrableAtFilter.eq_zero_of_tendsto
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
(h : MeasureTheory.IntegrableAtFilter f l μ)
(h' : ∀ s ∈ l, μ 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}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[TopologicalSpace β]
[BorelSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
:
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}
[MeasurableSpace α]
[TopologicalSpace α]
[TopologicalSpace.PseudoMetrizableSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
(h's : TopologicalSpace.IsSeparable s)
:
MeasureTheory.AEStronglyMeasurable f (μ.restrict 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}
[MeasurableSpace α]
[TopologicalSpace α]
[TopologicalSpace β]
[h : SecondCountableTopologyEither α β]
[OpensMeasurableSpace α]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
:
MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
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}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : IsCompact s)
(h's : MeasurableSet s)
:
MeasureTheory.AEStronglyMeasurable f (μ.restrict 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}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[TopologicalSpace.PseudoMetrizableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : α}
{t : Set α}
{f : α → E}
(hft : ContinuousOn f t)
(ht : MeasurableSet t)
(h't : TopologicalSpace.IsSeparable t)
(ha : a ∈ t)
:
MeasureTheory.IntegrableAtFilter f (nhdsWithin a t) μ
theorem
ContinuousOn.integrableAt_nhdsWithin
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[SecondCountableTopologyEither α E]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : α}
{t : Set α}
{f : α → E}
(hft : ContinuousOn f t)
(ht : MeasurableSet t)
(ha : a ∈ t)
:
MeasureTheory.IntegrableAtFilter f (nhdsWithin a t) μ
theorem
Continuous.integrableAt_nhds
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[SecondCountableTopologyEither α E]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : α → E}
(hf : Continuous f)
(a : α)
:
MeasureTheory.IntegrableAtFilter f (nhds a) μ
theorem
ContinuousOn.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : IsOpen s)
(hf : ContinuousOn f s)
(x : α)
:
x ∈ s → StronglyMeasurableAtFilter f (nhds x) μ
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}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopologyEither α E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : IsOpen s)
(hf : ∀ x ∈ s, ContinuousAt f x)
(x : α)
:
x ∈ s → StronglyMeasurableAtFilter f (nhds x) μ
theorem
Continuous.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
(hf : Continuous f)
(μ : MeasureTheory.Measure α)
(l : Filter α)
:
theorem
ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin
{α : Type u_5}
{β : Type u_6}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
(x : α)
:
StronglyMeasurableAtFilter f (nhdsWithin x s) μ
If a function is continuous on a measurable set s, then it is measurable at the filter
𝓝[s] x for all x.
Lemmas about adding and removing interval boundaries #
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}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
(ha : μ {a} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
theorem
integrableOn_Icc_iff_integrableOn_Ico'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
(hb : μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ
theorem
integrableOn_Ico_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
(ha : μ {a} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Ioc_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
(hb : μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Icc_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
(ha : μ {a} ≠ ⊤)
(hb : μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Ici_iff_integrableOn_Ioi'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
(hb : μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ
theorem
integrableOn_Iic_iff_integrableOn_Iio'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
(hb : μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ
theorem
integrableOn_Icc_iff_integrableOn_Ioc
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
theorem
integrableOn_Icc_iff_integrableOn_Ico
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ
theorem
integrableOn_Ico_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Ioc_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Icc_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
theorem
integrableOn_Ici_iff_integrableOn_Ioi
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ
theorem
integrableOn_Iic_iff_integrableOn_Iio
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ