mathlib documentation

measure_theory.integral.integrable_on

Functions integrable on a set and at a filter #

We define integrable_on f s μ := integrable f (μ.restrict s) and prove theorems like integrable_on_union : integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ.

Next we define a predicate integrable_at_filter (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 strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] (f : α → β) (l : filter α) (μ : measure_theory.measure α . "volume_tac") :
Prop

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
@[simp]
theorem strongly_measurable_at_bot {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] {μ : measure_theory.measure α} {f : α → β} :
@[protected]
theorem strongly_measurable_at_filter.eventually {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : strongly_measurable_at_filter f l μ) :
@[protected]
theorem strongly_measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] {l l' : filter α} {f : α → β} {μ : measure_theory.measure α} (h : strongly_measurable_at_filter f l μ) (h' : l' l) :
theorem ae_strongly_measurable.strongly_measurable_at_filter_of_mem {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} {s : set α} (h : measure_theory.ae_strongly_measurable f (μ.restrict s)) (hl : s l) :
theorem measure_theory.has_finite_integral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} {C : } (hs : μ s < ) (hf : ∀ᵐ (x : α) ∂μ.restrict s, f x C) :
def measure_theory.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] (f : α → E) (s : set α) (μ : measure_theory.measure α . "volume_tac") :
Prop

A function is integrable_on 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
theorem measure_theory.integrable_on.integrable {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) :
@[simp]
theorem measure_theory.integrable_on_empty {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} :
theorem measure_theory.integrable_on_zero {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {s : set α} {μ : measure_theory.measure α} :
measure_theory.integrable_on (λ (_x : α), 0) s μ
@[simp]
theorem measure_theory.integrable_on_const {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {s : set α} {μ : measure_theory.measure α} {C : E} :
measure_theory.integrable_on (λ (_x : α), C) s μ C = 0 μ s <
theorem measure_theory.integrable_on.mono {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ ν : measure_theory.measure α} (h : measure_theory.integrable_on f t ν) (hs : s t) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s t) :
theorem measure_theory.integrable_on.mono_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (h : measure_theory.integrable_on f s ν) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s ≤ᵐ[μ] t) :
theorem measure_theory.integrable_on.congr_set_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s =ᵐ[μ] t) :
theorem measure_theory.integrable_on.congr_fun' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f g : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hst : f =ᵐ[μ.restrict s] g) :
theorem measure_theory.integrable_on.congr_fun {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f g : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hst : set.eq_on f g s) (hs : measurable_set s) :
theorem measure_theory.integrable.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f μ) :
theorem measure_theory.integrable.integrable_on' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f (μ.restrict s)) :
theorem measure_theory.integrable_on.restrict {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hs : measurable_set s) :
theorem measure_theory.integrable_on.left_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f (s t) μ) :
theorem measure_theory.integrable_on.right_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f (s t) μ) :
theorem measure_theory.integrable_on.union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (hs : measure_theory.integrable_on f s μ) (ht : measure_theory.integrable_on f t μ) :
@[simp]
@[simp]
theorem measure_theory.integrable_on_singleton_iff {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} {x : α} [measurable_singleton_class α] :
@[simp]
theorem measure_theory.integrable_on_finite_bUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} {s : set β} (hs : s.finite) {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ
@[simp]
theorem measure_theory.integrable_on_finset_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} {s : finset β} {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ
@[simp]
theorem measure_theory.integrable_on_finite_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} [finite β] {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β), t i) μ ∀ (i : β), measure_theory.integrable_on f (t i) μ
theorem measure_theory.integrable_on.add_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (hμ : measure_theory.integrable_on f s μ) (hν : measure_theory.integrable_on f s ν) :
@[simp]
theorem measurable_embedding.integrable_on_map_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] [measurable_space β] {e : α → β} (he : measurable_embedding e) {f : β → E} {μ : measure_theory.measure α} {s : set β} :
theorem measure_theory.integrable_on_map_equiv {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] [measurable_space β] (e : α ≃ᵐ β) {f : β → E} {μ : measure_theory.measure α} {s : set β} :
theorem measure_theory.measure_preserving.integrable_on_comp_preimage {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {μ : measure_theory.measure α} [measurable_space β] {e : α → β} {ν : measure_theory.measure β . "volume_tac"} (h₁ : measure_theory.measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set β} :
theorem measure_theory.measure_preserving.integrable_on_image {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {μ : measure_theory.measure α} [measurable_space β] {e : α → β} {ν : measure_theory.measure β . "volume_tac"} (h₁ : measure_theory.measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set α} :
theorem measure_theory.integrable_on.indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hs : measurable_set s) :
theorem measure_theory.integrable.indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f μ) (hs : measurable_set s) :
theorem measure_theory.integrable_indicator_const_Lp {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {E : Type u_2} [normed_add_comm_group E] {p : ennreal} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :
theorem measure_theory.integrable_on_Lp_of_measure_ne_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {E : Type u_2} [normed_add_comm_group E] {p : ennreal} {s : set α} (f : (measure_theory.Lp E p μ)) (hp : 1 p) (hμs : μ s ) :
theorem measure_theory.integrable.lintegral_lt_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) :
∫⁻ (x : α), ennreal.of_real (f x) μ <
theorem measure_theory.integrable_on.set_lintegral_lt_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → } {s : set α} (hf : measure_theory.integrable_on f s μ) :
∫⁻ (x : α) in s, ennreal.of_real (f x) μ <
def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] (f : α → E) (l : filter α) (μ : measure_theory.measure α . "volume_tac") :
Prop

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.small_sets.

Equations
@[protected]
theorem measure_theory.integrable_at_filter.eventually {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} (h : measure_theory.integrable_at_filter f l μ) :
∀ᶠ (s : set α) in l.small_sets, measure_theory.integrable_on f s μ
theorem measure_theory.integrable_at_filter.filter_mono {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hl : l l') (hl' : measure_theory.integrable_at_filter f l' μ) :

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 continuous_on.ae_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space α] [opens_measurable_space α] [measurable_space β] [topological_space β] [borel_space β] {f : α → β} {s : set α} {μ : measure_theory.measure α} (hf : continuous_on f s) (hs : measurable_set s) :

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

A function which is continuous on a separable set s is almost everywhere strongly measurable with respect to μ.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.

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 continuous_at.strongly_measurable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] [topological_space α] [opens_measurable_space α] [second_countable_topology_either α E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (hs : is_open s) (hf : ∀ (x : α), x scontinuous_at f x) (x : α) (H : x s) :

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