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
measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β)
(l : filter α)
(μ : measure_theory.measure α . "volume_tac") :
Prop
A function f is measurable at filter l w.r.t. a measure μ if it is ae-measurable
w.r.t. μ.restrict s for some s ∈ l.
Equations
- measurable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), ae_measurable f (measure_theory.measure.restrict μ s)
@[simp]
theorem
measurable_at_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β} :
@[protected]
theorem
measurable_at_filter.eventually
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measurable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, ae_measurable f (μ.restrict s)
@[protected]
theorem
measurable_at_filter.filter_mono
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l l' : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measurable_at_filter f l μ)
(h' : l' ≤ l) :
measurable_at_filter f l' μ
@[protected]
theorem
ae_measurable.measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : ae_measurable f μ) :
measurable_at_filter f l μ
theorem
ae_measurable.measurable_at_filter_of_mem
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
{s : set α}
(h : ae_measurable f (μ.restrict s))
(hl : s ∈ l) :
measurable_at_filter f l μ
@[protected]
theorem
measurable.measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measurable f) :
measurable_at_filter f l μ
theorem
measure_theory.has_finite_integral_restrict_of_bounded
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_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_group E]
[measurable_space E]
(f : α → E)
(s : set α)
(μ : measure_theory.measure α . "volume_tac") :
Prop
A function is integrable_on a set s if it is almost everywhere 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_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ) :
measure_theory.integrable f (μ.restrict s)
@[simp]
theorem
measure_theory.integrable_on_empty
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.integrable_on_univ
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α} :
theorem
measure_theory.integrable_on_zero
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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_group E]
[measurable_space E]
{s : set α}
{μ : measure_theory.measure α}
{C : E} :
theorem
measure_theory.integrable_on.mono
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ)
(hs : measurable_set s) :
measure_theory.integrable_on f s (μ.restrict t)
theorem
measure_theory.integrable_on.left_of_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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_group E]
[measurable_space 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_group E]
[measurable_space E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α}
(hs : measure_theory.integrable_on f s μ)
(ht : measure_theory.integrable_on f t μ) :
measure_theory.integrable_on f (s ∪ t) μ
@[simp]
theorem
measure_theory.integrable_on_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f (s ∪ t) μ ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f t μ
@[simp]
theorem
measure_theory.integrable_on_singleton_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{x : α}
[measurable_singleton_class α] :
@[simp]
theorem
measure_theory.integrable_on_finite_Union
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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 ∈ s → measure_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_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{s : finset β}
{t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i ∈ s), t i) μ ↔ ∀ (i : β), i ∈ s → measure_theory.integrable_on f (t i) μ
@[simp]
theorem
measure_theory.integrable_on_fintype_Union
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
[fintype β]
{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_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α}
(hμ : measure_theory.integrable_on f s μ)
(hν : measure_theory.integrable_on f s ν) :
measure_theory.integrable_on f s (μ + ν)
@[simp]
theorem
measure_theory.integrable_on_add_measure
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f s (μ + ν) ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f s ν
theorem
measurable_embedding.integrable_on_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
[measurable_space β]
{e : α → β}
(he : measurable_embedding e)
{f : β → E}
{μ : measure_theory.measure α}
{s : set β} :
measure_theory.integrable_on f s (⇑(measure_theory.measure.map e) μ) ↔ measure_theory.integrable_on (f ∘ e) (e ⁻¹' s) μ
theorem
measure_theory.integrable_on_map_equiv
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
[measurable_space β]
(e : α ≃ᵐ β)
{f : β → E}
{μ : measure_theory.measure α}
{s : set β} :
measure_theory.integrable_on f s (⇑(measure_theory.measure.map ⇑e) μ) ↔ measure_theory.integrable_on (f ∘ ⇑e) (⇑e ⁻¹' s) μ
theorem
measure_theory.measure_preserving.integrable_on_comp_preimage
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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 β} :
measure_theory.integrable_on (f ∘ e) (e ⁻¹' s) μ ↔ measure_theory.integrable_on f s ν
theorem
measure_theory.measure_preserving.integrable_on_image
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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 α} :
measure_theory.integrable_on f (e '' s) ν ↔ measure_theory.integrable_on (f ∘ e) s μ
theorem
measure_theory.integrable_indicator_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ ↔ measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.indicator
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ)
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable.indicator
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable f μ)
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable_indicator_const_Lp
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E]
{p : ℝ≥0∞}
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : E) :
measure_theory.integrable ⇑(measure_theory.indicator_const_Lp p hs hμs c) μ
theorem
measure_theory.integrable_on_Lp_of_measure_ne_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E]
{p : ℝ≥0∞}
{s : set α}
(f : ↥(measure_theory.Lp E p μ))
(hp : 1 ≤ p)
(hμs : ⇑μ s ≠ ⊤) :
def
measure_theory.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space 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.lift' powerset.
Equations
- measure_theory.integrable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), measure_theory.integrable_on f s μ
@[protected]
theorem
measure_theory.integrable_at_filter.eventually
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
(h : measure_theory.integrable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_at_filter.filter_mono
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : l ≤ l')
(hl' : measure_theory.integrable_at_filter f l' μ) :
theorem
measure_theory.integrable_at_filter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : measure_theory.integrable_at_filter f l μ) :
measure_theory.integrable_at_filter f (l ⊓ l') μ
theorem
measure_theory.integrable_at_filter.inf_of_right
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : measure_theory.integrable_at_filter f l μ) :
measure_theory.integrable_at_filter f (l' ⊓ l) μ
@[simp]
theorem
measure_theory.integrable_at_filter.inf_ae_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
measure_theory.integrable_at_filter f (l ⊓ μ.ae) μ ↔ measure_theory.integrable_at_filter f l μ
theorem
measure_theory.integrable_at_filter.of_inf_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
measure_theory.integrable_at_filter f (l ⊓ μ.ae) μ → measure_theory.integrable_at_filter f l μ
Alias of integrable_at_filter.inf_ae_iff.
theorem
measure_theory.measure.finite_at_filter.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
(hf : filter.is_bounded_under has_le.le 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
measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f (l ⊓ μ.ae) (𝓝 b)) :
theorem
filter.tendsto.integrable_at_filter_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f (l ⊓ μ.ae) (𝓝 b)) :
Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto_ae.
theorem
measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f l (𝓝 b)) :
theorem
filter.tendsto.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f l (𝓝 b)) :
Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto.
theorem
measure_theory.integrable_add_of_disjoint
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{μ : measure_theory.measure α}
[borel_space E]
[topological_space.second_countable_topology E]
{f g : α → E}
(h : disjoint (function.support f) (function.support g))
(hf : measurable f)
(hg : measurable g) :
measure_theory.integrable (f + g) μ ↔ measure_theory.integrable f μ ∧ measure_theory.integrable g μ
theorem
is_compact.integrable_on_of_nhds_within
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : is_compact s)
{f : α → E}
(hf : ∀ (x : α), x ∈ s → measure_theory.integrable_at_filter f (𝓝[s] x) μ) :
If a function is integrable at 𝓝[s] x for each point x of a compact set s, then it is
integrable on s.
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) :
ae_measurable f (μ.restrict s)
A function which is continuous on a set s is almost everywhere measurable with respect to
μ.restrict s.
theorem
continuous_on.integrable_at_nhds_within
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{a : α}
{t : set α}
{f : α → E}
(hft : continuous_on f t)
(ht : measurable_set t)
(ha : a ∈ t) :
measure_theory.integrable_at_filter f (𝓝[t] a) μ
theorem
continuous_on.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[borel_space E]
[t2_space α]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hf : continuous_on f s) :
A function f continuous on a compact set s is integrable on this set with respect to any
locally finite measure.
theorem
continuous_on.integrable_on_Icc
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[preorder β]
[topological_space β]
[t2_space β]
[compact_Icc_space β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous_on f (set.Icc a b)) :
measure_theory.integrable_on f (set.Icc a b) μ
theorem
continuous_on.integrable_on_interval
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous_on f [a, b]) :
measure_theory.integrable_on f [a, b] μ
theorem
continuous.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hf : continuous f) :
A continuous function f is integrable on any compact set with respect to any locally finite
measure.
theorem
continuous.integrable_on_Icc
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[preorder β]
[topological_space β]
[t2_space β]
[compact_Icc_space β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous f) :
measure_theory.integrable_on f (set.Icc a b) μ
theorem
continuous.integrable_on_Ioc
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous f) :
measure_theory.integrable_on f (set.Ioc a b) μ
theorem
continuous.integrable_on_interval
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous f) :
measure_theory.integrable_on f [a, b] μ
theorem
continuous.integrable_on_interval_oc
{β : Type u_2}
{E : Type u_3}
[measurable_space E]
[normed_group E]
[borel_space E]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[measurable_space β]
[opens_measurable_space β]
{μ : measure_theory.measure β}
[measure_theory.is_locally_finite_measure μ]
{a b : β}
{f : β → E}
(hf : continuous f) :
measure_theory.integrable_on f (Ι a b) μ
theorem
continuous.integrable_of_compact_closure_support
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{f : α → E}
(hf : continuous f)
(hfc : is_compact (closure (function.support f))) :
A continuous function with compact closure of the support is integrable on the whole space.
theorem
measure_theory.integrable_on.mul_continuous_on_of_subset
{α : Type u_1}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
{f g : α → ℝ}
(hf : measure_theory.integrable_on f s μ)
(hg : continuous_on g t)
(hs : measurable_set s)
(ht : is_compact t)
(hst : s ⊆ t) :
measure_theory.integrable_on (λ (x : α), (f x) * g x) s μ
theorem
measure_theory.integrable_on.mul_continuous_on
{α : Type u_1}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{f g : α → ℝ}
[t2_space α]
(hf : measure_theory.integrable_on f s μ)
(hg : continuous_on g s)
(hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (f x) * g x) s μ
theorem
measure_theory.integrable_on.continuous_on_mul_of_subset
{α : Type u_1}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
{f g : α → ℝ}
(hf : measure_theory.integrable_on f s μ)
(hg : continuous_on g t)
(hs : measurable_set s)
(ht : is_compact t)
(hst : s ⊆ t) :
measure_theory.integrable_on (λ (x : α), (g x) * f x) s μ
theorem
measure_theory.integrable_on.continuous_on_mul
{α : Type u_1}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{f g : α → ℝ}
[t2_space α]
(hf : measure_theory.integrable_on f s μ)
(hg : continuous_on g s)
(hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (g x) * f x) s μ
theorem
monotone_on.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[borel_space α]
[borel_space E]
[conditionally_complete_linear_order α]
[conditionally_complete_linear_order E]
[order_topology α]
[order_topology E]
[topological_space.second_countable_topology E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hmono : monotone_on f s) :
theorem
antitone_on.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[borel_space α]
[borel_space E]
[conditionally_complete_linear_order α]
[conditionally_complete_linear_order E]
[order_topology α]
[order_topology E]
[topological_space.second_countable_topology E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hanti : antitone_on f s) :
theorem
monotone.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[borel_space α]
[borel_space E]
[conditionally_complete_linear_order α]
[conditionally_complete_linear_order E]
[order_topology α]
[order_topology E]
[topological_space.second_countable_topology E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hmono : monotone f) :
theorem
antitone.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[borel_space α]
[borel_space E]
[conditionally_complete_linear_order α]
[conditionally_complete_linear_order E]
[order_topology α]
[order_topology E]
[topological_space.second_countable_topology E]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hanti : antitone f) :