Borel (measurable) space
Main definitions
borel α: the leastσ-algebra that contains all open sets;class borel_space: a space withtopological_spaceandmeasurable_spacestructures such that‹measurable_space α› = borel α;class opens_measurable_space: a space withtopological_spaceandmeasurable_spacestructures such that all open sets are measurable; equivalently,borel α ≤ ‹measurable_space α›.borel_spaceinstances onempty,unit,bool,nat,int,rat;measurableandborel_spaceinstances onℝ,ℝ≥0,ennreal.- A measure is
regularif it is finite on compact sets, inner regular and outer regular.
Main statements
is_open.is_measurable,is_closed.is_measurable: open and closed sets are measurable;continuous.measurable: a continuous function is measurable;continuous.measurable2: iff : α → βandg : α → γare measurable andop : β × γ → δis continuous, thenλ x, op (f x, g y)is measurable;measurable.addetc : dot notation for arithmetic operations onmeasurablepredicates, and similarly fordistandedist;measurable.ennreal*: special cases for arithmetic operations onennreals.
measurable_space structure generated by topological_space.
Equations
- borel α = measurable_space.generate_from {s : set α | is_open s}
theorem
borel_eq_generate_from_of_subbasis
{α : Type u_1}
{s : set (set α)}
[t : topological_space α]
[topological_space.second_countable_topology α]
(hs : t = topological_space.generate_from s) :
theorem
borel_eq_generate_Iio
(α : Type u_1)
[topological_space α]
[topological_space.second_countable_topology α]
[linear_order α]
[order_topology α] :
theorem
borel_eq_generate_Ioi
(α : Type u_1)
[topological_space α]
[topological_space.second_countable_topology α]
[linear_order α]
[order_topology α] :
theorem
borel_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{t : topological_space β} :
borel α = measurable_space.comap f (borel β)
theorem
continuous.borel_measurable
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f) :
@[class]
structure
opens_measurable_space
(α : Type u_5)
[topological_space α]
[h : measurable_space α] :
Prop
A space with measurable_space and topological_space structures such that
all open sets are measurable.
@[class]
A space with measurable_space and topological_space structures such that
the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.
@[instance]
def
borel_space.opens_measurable
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α] :
In a borel_space all open sets are measurable.
@[instance]
def
subtype.borel_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[hα : borel_space α]
(s : set α) :
@[instance]
def
subtype.opens_measurable_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[h : opens_measurable_space α]
(s : set α) :
theorem
is_open.is_measurable
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(h : is_open s) :
theorem
is_measurable_interior
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
theorem
is_closed.is_measurable
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(h : is_closed s) :
theorem
is_compact.is_measurable
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t2_space α]
(h : is_compact s) :
theorem
is_measurable_closure
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
is_measurable (closure s)
theorem
measurable_of_is_open
{γ : Type u_3}
{δ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_open s → is_measurable (f ⁻¹' s)) :
theorem
measurable_of_is_closed
{γ : Type u_3}
{δ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_closed s → is_measurable (f ⁻¹' s)) :
theorem
measurable_of_is_closed'
{γ : Type u_3}
{δ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_closed s → s.nonempty → s ≠ set.univ → is_measurable (f ⁻¹' s)) :
@[instance]
def
nhds_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(a : α) :
theorem
is_measurable.nhds_within_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
{s : set α}
(hs : is_measurable s)
(a : α) :
If s is a measurable set, then 𝓝[s] a is a measurably generated filter for
each a. This cannot be an instance because it depends on a non-instance hs : is_measurable s.
@[instance]
def
opens_measurable_space.to_measurable_singleton_class
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t1_space α] :
@[instance]
def
prod.opens_measurable_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space β]
[measurable_space β]
[opens_measurable_space β]
[topological_space.second_countable_topology α]
[topological_space.second_countable_topology β] :
opens_measurable_space (α × β)
theorem
is_measurable_Ici
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Ici a)
theorem
is_measurable_Iic
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Iic a)
theorem
is_measurable_Icc
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.Icc a b)
@[instance]
def
nhds_within_Ici_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
@[instance]
def
nhds_within_Iic_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
@[instance]
def
at_top_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
@[instance]
def
at_bot_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
theorem
is_measurable_le'
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[partial_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α] :
is_measurable {p : α × α | p.fst ≤ p.snd}
theorem
is_measurable_le
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[partial_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(hf : measurable f)
(hg : measurable g) :
is_measurable {a : δ | f a ≤ g a}
theorem
is_measurable_Iio
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Iio a)
theorem
is_measurable_Ioi
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Ioi a)
theorem
is_measurable_Ioo
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.Ioo a b)
theorem
is_measurable_Ioc
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.Ioc a b)
theorem
is_measurable_Ico
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.Ico a b)
@[instance]
def
nhds_within_Ioi_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
@[instance]
def
nhds_within_Iio_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
theorem
is_measurable_lt'
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α] :
is_measurable {p : α × α | p.fst < p.snd}
theorem
is_measurable_lt
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(hf : measurable f)
(hg : measurable g) :
is_measurable {a : δ | f a < g a}
theorem
is_measurable_interval
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[decidable_linear_order α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.interval a b)
theorem
measurable.max
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[decidable_linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : δ), max (f a) (g a))
theorem
measurable.min
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[decidable_linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : δ), min (f a) (g a))
theorem
continuous.measurable
{α : Type u_1}
{γ : Type u_3}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
{f : α → γ}
(hf : continuous f) :
A continuous function from an opens_measurable_space to a borel_space
is measurable.
def
homeomorph.to_measurable_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
(h : α ≃ₜ β) :
measurable_equiv α β
A homeomorphism between two Borel spaces is a measurable equivalence.
Equations
- h.to_measurable_equiv = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
theorem
measurable_of_continuous_on_compl_singleton
{α : Type u_1}
{γ : Type u_3}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[t1_space α]
{f : α → γ}
(a : α)
(hf : continuous_on f {x : α | x ≠ a}) :
theorem
continuous.measurable2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space β]
[measurable_space β]
[opens_measurable_space β]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
[topological_space.second_countable_topology α]
[topological_space.second_countable_topology β]
{f : δ → α}
{g : δ → β}
{c : α → β → γ}
(h : continuous (λ (p : α × β), c p.fst p.snd))
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : δ), c (f a) (g a))
theorem
measurable.smul
{α : Type u_1}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
[semiring α]
[topological_space.second_countable_topology α]
[add_comm_monoid γ]
[topological_space.second_countable_topology γ]
[semimodule α γ]
[topological_semimodule α γ]
{f : δ → α}
{g : δ → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (c : δ), f c • g c)
theorem
measurable.const_smul
{δ : Type u_4}
[measurable_space δ]
{R : Type u_1}
{M : Type u_2}
[topological_space R]
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[topological_space M]
[topological_semimodule R M]
[measurable_space M]
[borel_space M]
{f : δ → M}
(hf : measurable f)
(c : R) :
measurable (λ (x : δ), c • f x)
theorem
measurable_const_smul_iff
{γ : Type u_3}
{δ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{α : Type u_1}
[topological_space α]
[division_ring α]
[add_comm_monoid γ]
[semimodule α γ]
[topological_semimodule α γ]
{f : δ → γ}
{c : α}
(hc : c ≠ 0) :
measurable (λ (x : δ), c • f x) ↔ measurable f
theorem
measurable.const_mul
{δ : Type u_4}
[measurable_space δ]
{R : Type u_1}
[topological_space R]
[measurable_space R]
[borel_space R]
[semiring R]
[topological_semiring R]
{f : δ → R}
(hf : measurable f)
(c : R) :
measurable (λ (x : δ), c * f x)
theorem
measurable.mul_const
{δ : Type u_4}
[measurable_space δ]
{R : Type u_1}
[topological_space R]
[measurable_space R]
[borel_space R]
[semiring R]
[topological_semiring R]
{f : δ → R}
(hf : measurable f)
(c : R) :
measurable (λ (x : δ), (f x) * c)
theorem
prod_le_borel_prod
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β] :
prod.measurable_space ≤ borel (α × β)
@[instance]
def
prod.borel_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology α]
[topological_space.second_countable_topology β] :
borel_space (α × β)
theorem
measurable_mul
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), (p.fst) * p.snd)
theorem
measurable_add
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_add α]
[has_continuous_add α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), p.fst + p.snd)
theorem
measurable.add
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_add α]
[has_continuous_add α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(a : measurable f)
(a_1 : measurable g) :
measurable (λ (a : δ), f a + g a)
theorem
measurable.mul
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_mul α]
[has_continuous_mul α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(a : measurable f)
(a_1 : measurable g) :
measurable (λ (a : δ), (f a) * g a)
theorem
measurable.add'
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_add α]
[has_continuous_add α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(a : measurable f)
(a_1 : measurable g) :
measurable (f + g)
theorem
measurable.mul'
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_mul α]
[has_continuous_mul α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(a : measurable f)
(a_1 : measurable g) :
measurable (f * g)
A variant of measurable.mul that uses * on functions
theorem
measurable_mul_left
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_mul α]
[has_continuous_mul α]
(x : α) :
measurable (λ (y : α), x * y)
theorem
measurable_add_left
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_add α]
[has_continuous_add α]
(x : α) :
measurable (λ (y : α), x + y)
theorem
measurable_mul_right
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_mul α]
[has_continuous_mul α]
(x : α) :
measurable (λ (y : α), y * x)
theorem
measurable_add_right
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_add α]
[has_continuous_add α]
(x : α) :
measurable (λ (y : α), y + x)
theorem
finset.measurable_sum
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
{ι : Type u_2}
[add_comm_monoid α]
[has_continuous_add α]
[topological_space.second_countable_topology α]
{f : ι → δ → α}
(s : finset ι)
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (a : δ), ∑ (i : ι) in s, f i a)
theorem
finset.measurable_prod
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
{ι : Type u_2}
[comm_monoid α]
[has_continuous_mul α]
[topological_space.second_countable_topology α]
{f : ι → δ → α}
(s : finset ι)
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (a : δ), ∏ (i : ι) in s, f i a)
theorem
measurable_inv
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[group α]
[topological_group α] :
theorem
measurable_neg
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α]
[add_group α]
[topological_add_group α] :
theorem
measurable.inv
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[group α]
[topological_group α]
{f : δ → α}
(hf : measurable f) :
measurable (λ (a : δ), (f a)⁻¹)
theorem
measurable.neg
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
{f : δ → α}
(hf : measurable f) :
measurable (λ (a : δ), -f a)
theorem
measurable.inv'
{δ : Type u_4}
[measurable_space δ]
{α : Type u_1}
[normed_field α]
[measurable_space α]
[borel_space α]
{f : δ → α}
(hf : measurable f) :
measurable (λ (a : δ), (f a)⁻¹)
theorem
measurable.of_neg
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
{f : δ → α}
(hf : measurable (λ (a : δ), -f a)) :
theorem
measurable.of_inv
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[group α]
[topological_group α]
{f : δ → α}
(hf : measurable (λ (a : δ), (f a)⁻¹)) :
@[simp]
theorem
measurable_inv_iff
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[group α]
[topological_group α]
{f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹) ↔ measurable f
@[simp]
theorem
measurable_neg_iff
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
{f : δ → α} :
measurable (λ (a : δ), -f a) ↔ measurable f
theorem
measurable.sub
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
[topological_space.second_countable_topology α]
{f g : δ → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (x : δ), f x - g x)
theorem
measurable_comp_iff_of_closed_embedding
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space β]
[measurable_space β]
[borel_space β]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → β}
(g : β → γ)
(hg : closed_embedding g) :
measurable (g ∘ f) ↔ measurable f
theorem
measurable_of_Iio
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), is_measurable (f ⁻¹' set.Iio x)) :
theorem
measurable_of_Ioi
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), is_measurable (f ⁻¹' set.Ioi x)) :
theorem
measurable_of_Iic
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), is_measurable (f ⁻¹' set.Iic x)) :
theorem
measurable_of_Ici
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), is_measurable (f ⁻¹' set.Ici x)) :
theorem
measurable.is_lub
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
[encodable ι]
{f : ι → δ → α}
{g : δ → α}
(hf : ∀ (i : ι), measurable (f i))
(hg : ∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem
measurable.is_glb
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
[encodable ι]
{f : ι → δ → α}
{g : δ → α}
(hf : ∀ (i : ι), measurable (f i))
(hg : ∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem
measurable.supr_Prop
{δ : Type u_4}
[measurable_space δ]
{α : Type u_1}
[measurable_space α]
[complete_lattice α]
(p : Prop)
{f : δ → α}
(hf : measurable f) :
measurable (λ (b : δ), ⨆ (h : p), f b)
theorem
measurable.infi_Prop
{δ : Type u_4}
[measurable_space δ]
{α : Type u_1}
[measurable_space α]
[complete_lattice α]
(p : Prop)
{f : δ → α}
(hf : measurable f) :
measurable (λ (b : δ), ⨅ (h : p), f b)
theorem
measurable_supr
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
[encodable ι]
{f : ι → δ → α}
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨆ (i : ι), f i b)
theorem
measurable_infi
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
[encodable ι]
{f : ι → δ → α}
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨅ (i : ι), f i b)
theorem
measurable_bsupr
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
(s : set ι)
{f : ι → δ → α}
(hs : s.countable)
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨆ (i : ι) (H : i ∈ s), f i b)
theorem
measurable_binfi
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
(s : set ι)
{f : ι → δ → α}
(hs : s.countable)
(hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨅ (i : ι) (H : i ∈ s), f i b)
theorem
measurable_cSup
{α : Type u_1}
{δ : Type u_4}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[conditionally_complete_linear_order α]
[topological_space.second_countable_topology α]
[order_topology α]
{ι : Type u_2}
{f : ι → δ → α}
{s : set ι}
(hs : s.countable)
(hf : ∀ (i : ι), measurable (f i))
(bdd : ∀ (x : δ), bdd_above ((λ (i : ι), f i x) '' s)) :
measurable (λ (x : δ), Sup ((λ (i : ι), f i x) '' s))
def
homemorph.to_measurable_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
(h : α ≃ₜ β) :
measurable_equiv α β
Convert a homeomorph to a measurable_equiv.
Equations
- homemorph.to_measurable_equiv h = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem
is_measurable_ball
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ} :
is_measurable (metric.ball x ε)
theorem
is_measurable_closed_ball
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ} :
theorem
measurable_inf_dist
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{s : set α} :
measurable (λ (x : α), metric.inf_dist x s)
theorem
measurable.inf_dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α} :
measurable (λ (x : β), metric.inf_dist (f x) s)
theorem
measurable_dist
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), dist p.fst p.snd)
theorem
measurable.dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
[topological_space.second_countable_topology α]
{f g : β → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (b : β), dist (f b) (g b))
theorem
measurable_nndist
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), nndist p.fst p.snd)
theorem
measurable.nndist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
[topological_space.second_countable_topology α]
{f g : β → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (b : β), nndist (f b) (g b))
theorem
is_measurable_eball
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ennreal} :
is_measurable (emetric.ball x ε)
theorem
measurable_edist_right
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α} :
measurable (edist x)
theorem
measurable_edist_left
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α} :
measurable (λ (y : α), edist y x)
theorem
measurable_inf_edist
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{s : set α} :
measurable (λ (x : α), emetric.inf_edist x s)
theorem
measurable.inf_edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α} :
measurable (λ (x : β), emetric.inf_edist (f x) s)
theorem
measurable_edist
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), edist p.fst p.snd)
theorem
measurable.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
[topological_space.second_countable_topology α]
{f g : β → α}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (b : β), edist (f b) (g b))
theorem
measurable.sub_nnreal
{α : Type u_1}
[measurable_space α]
{f g : α → ℝ≥0}
(a : measurable f)
(a_1 : measurable g) :
measurable (λ (a : α), f a - g a)
theorem
measurable.nnreal_of_real
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), nnreal.of_real (f x))
theorem
measurable.nnreal_coe
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0}
(hf : measurable f) :
measurable (λ (x : α), ↑(f x))
theorem
measurable.ennreal_coe
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0}
(hf : measurable f) :
measurable (λ (x : α), ↑(f x))
theorem
measurable.ennreal_of_real
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), ennreal.of_real (f x))
The set of finite ennreal numbers is measurable_equiv to nnreal.
theorem
ennreal.measurable_of_measurable_nnreal
{α : Type u_1}
[measurable_space α]
{f : ennreal → α}
(h : measurable (λ (p : ℝ≥0), f ↑p)) :
ennreal is measurable_equiv to nnreal ⊕ unit.
Equations
- ennreal.ennreal_equiv_sum = {to_equiv := {to_fun := (equiv.option_equiv_sum_punit ℝ≥0).to_fun, inv_fun := (equiv.option_equiv_sum_punit ℝ≥0).inv_fun, left_inv := ennreal.ennreal_equiv_sum._proof_1, right_inv := ennreal.ennreal_equiv_sum._proof_2}, measurable_to_fun := ennreal.ennreal_equiv_sum._proof_3, measurable_inv_fun := ennreal.ennreal_equiv_sum._proof_4}
theorem
ennreal.measurable_of_measurable_nnreal_prod
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
{f : ennreal × β → γ}
(H₁ : measurable (λ (p : ℝ≥0 × β), f (↑(p.fst), p.snd)))
(H₂ : measurable (λ (x : β), f (⊤, x))) :
theorem
ennreal.measurable_of_measurable_nnreal_nnreal
{β : Type u_2}
[measurable_space β]
{f : ennreal × ennreal → β}
(h₁ : measurable (λ (p : ℝ≥0 × ℝ≥0), f (↑(p.fst), ↑(p.snd))))
(h₂ : measurable (λ (r : ℝ≥0), f (⊤, ↑r)))
(h₃ : measurable (λ (r : ℝ≥0), f (↑r, ⊤))) :
theorem
measurable.to_nnreal
{α : Type u_1}
[measurable_space α]
{f : α → ennreal}
(hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
theorem
measurable_ennreal_coe_iff
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0} :
measurable (λ (x : α), ↑(f x)) ↔ measurable f
theorem
measurable.to_real
{α : Type u_1}
[measurable_space α]
{f : α → ennreal}
(hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
theorem
measurable.ennreal_mul
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), (f a) * g a)
theorem
measurable.ennreal_add
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), f a + g a)
theorem
measurable.ennreal_sub
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), f a - g a)
theorem
measurable.ennreal_tsum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
[encodable ι]
{f : ι → α → ennreal}
(h : ∀ (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)
note: ennreal can probably be generalized in a future version of this lemma.
theorem
measurable_norm
{α : Type u_1}
[measurable_space α]
[normed_group α]
[opens_measurable_space α] :
theorem
measurable.norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f) :
measurable (λ (a : β), ∥f a∥)
theorem
measurable_nnnorm
{α : Type u_1}
[measurable_space α]
[normed_group α]
[opens_measurable_space α] :
theorem
measurable.nnnorm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f) :
measurable (λ (a : β), nnnorm (f a))
theorem
measurable_ennnorm
{α : Type u_1}
[measurable_space α]
[normed_group α]
[opens_measurable_space α] :
measurable (λ (x : α), ↑(nnnorm x))
theorem
measurable.ennnorm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f) :
measurable (λ (a : β), ↑(nnnorm (f a)))
theorem
continuous_linear_map.measurable
{𝕜 : Type u_5}
[normed_field 𝕜]
{E : Type u_6}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[opens_measurable_space E]
{F : Type u_7}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space F]
[borel_space F]
(L : E →L[𝕜] F) :
theorem
continuous_linear_map.measurable_comp
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_5}
[normed_field 𝕜]
{E : Type u_6}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[opens_measurable_space E]
{F : Type u_7}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space F]
[borel_space F]
(L : E →L[𝕜] F)
{φ : α → E}
(φ_meas : measurable φ) :
measurable (λ (a : α), ⇑L (φ a))
theorem
measurable_smul_const
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_5}
[nondiscrete_normed_field 𝕜]
[complete_space 𝕜]
[measurable_space 𝕜]
[borel_space 𝕜]
{E : Type u_6}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[borel_space E]
{f : α → 𝕜}
{c : E}
(hc : c ≠ 0) :
measurable (λ (x : α), f x • c) ↔ measurable f
structure
measure_theory.measure.regular
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α) :
Prop
- lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → ⇑μ K < ⊤
- outer_regular : ∀ ⦃A : set α⦄, is_measurable A → (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), ⇑μ U) ≤ ⇑μ A
- inner_regular : ∀ ⦃U : set α⦄, is_open U → (⇑μ U ≤ ⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), ⇑μ K)
A measure μ is regular if
- it is finite on all compact sets;
- it is outer regular:
μ(A) = inf { μ(U) | A ⊆ U open }forAmeasurable; - it is inner regular:
μ(U) = sup { μ(K) | K ⊆ U compact }forUopen.
theorem
measure_theory.measure.regular.outer_regular_eq
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
⦃A : set α⦄
(hA : is_measurable A) :
theorem
measure_theory.measure.regular.inner_regular_eq
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
⦃U : set α⦄
(hU : is_open U) :
theorem
measure_theory.measure.regular.map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[measurable_space β]
[topological_space β]
[t2_space β]
[borel_space β]
{μ : measure_theory.measure α}
(hμ : μ.regular)
(f : α ≃ₜ β) :
(⇑(measure_theory.measure.map ⇑f) μ).regular
theorem
measure_theory.measure.regular.smul
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
{x : ennreal}
(hx : x < ⊤) :