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}
{s : set (set α)}
[t : topological_space α]
[topological_space.second_countable_topology α] :
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 α]
[h : topological_space.second_countable_topology α]
[linear_order α]
[order_topology α] :
theorem
borel_comap
{α : Type u}
{β : Type v}
{f : α → β}
{t : topological_space β} :
borel α = measurable_space.comap f (borel β)
theorem
continuous.borel_measurable
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β} :
continuous f → measurable f
@[class]
structure
opens_measurable_space
(α : Type u_1)
[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.
Equations
@[instance]
def
subtype.borel_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[hα : borel_space α]
(s : set α) :
Equations
- _ = _
@[instance]
def
subtype.opens_measurable_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[h : opens_measurable_space α]
(s : set α) :
Equations
- _ = _
theorem
is_open.is_measurable
{α : Type u}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
is_open s → is_measurable s
theorem
is_measurable_interior
{α : Type u}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
theorem
is_closed.is_measurable
{α : Type u}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
is_closed s → is_measurable s
theorem
is_compact.is_measurable
{α : Type u}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t2_space α] :
is_compact s → is_measurable s
theorem
is_measurable_closure
{α : Type u}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
is_measurable (closure s)
@[instance]
def
nhds_is_measurably_generated
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(a : α) :
Equations
- _ = _
theorem
is_measurable.nhds_within_is_measurably_generated
{α : Type u}
[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}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t1_space α] :
theorem
is_measurable_Ici
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Ici a)
theorem
is_measurable_Iic
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Iic a)
theorem
is_measurable_Icc
{α : Type u}
[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}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
Equations
@[instance]
def
nhds_within_Iic_is_measurably_generated
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
Equations
@[instance]
def
at_top_is_measurably_generated
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
@[instance]
def
at_bot_is_measurably_generated
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
theorem
is_measurable_Iio
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Iio a)
theorem
is_measurable_Ioi
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
is_measurable (set.Ioi a)
theorem
is_measurable_Ioo
{α : Type u}
[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}
[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}
[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}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
Equations
@[instance]
def
nhds_within_Iio_is_measurably_generated
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
Equations
theorem
is_measurable_interval
{α : Type u}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[decidable_linear_order α]
[order_closed_topology α]
{a b : α} :
is_measurable (set.interval a b)
@[instance]
def
prod.opens_measurable_space
{α : Type u}
{β : Type v}
[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 (α × β)
Equations
theorem
continuous.measurable
{α : Type u}
{γ : Type w}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
{f : α → γ} :
continuous f → measurable 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 β] :
α ≃ₜ β → 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}
{γ : Type w}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[t1_space α]
{f : α → γ}
(a : α) :
continuous_on f {x : α | x ≠ a} → measurable f
theorem
continuous.measurable2
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[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 : α → β → γ} :
continuous (λ (p : α × β), c p.fst p.snd) → measurable f → measurable g → measurable (λ (a : δ), c (f a) (g a))
theorem
measurable.smul
{α : Type u}
{γ : Type w}
{δ : Type x}
[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 : δ → γ} :
measurable f → measurable g → measurable (λ (c : δ), f c • g c)
theorem
measurable.const_smul
{γ : Type w}
{δ : Type x}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{α : Type u_1}
[topological_space α]
[semiring α]
[add_comm_monoid γ]
[semimodule α γ]
[topological_semimodule α γ]
{f : δ → γ}
(hf : measurable f)
(c : α) :
measurable (λ (x : δ), c • f x)
theorem
measurable_const_smul_iff
{γ : Type w}
{δ : Type x}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{α : Type u_1}
[topological_space α]
[division_ring α]
[add_comm_monoid γ]
[semimodule α γ]
[topological_semimodule α γ]
{f : δ → γ}
{c : α} :
c ≠ 0 → (measurable (λ (x : δ), c • f x) ↔ measurable f)
theorem
is_measurable_le'
{α : Type u}
[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}
{δ : Type x}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[partial_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → is_measurable {a : δ | f a ≤ g a}
theorem
measurable.max
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[decidable_linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), max (f a) (g a))
theorem
measurable.min
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[decidable_linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), min (f a) (g a))
theorem
prod_le_borel_prod
{α : Type u}
{β : Type v}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β] :
prod.measurable_space ≤ borel (α × β)
@[instance]
def
prod.borel_space
{α : Type u}
{β : Type v}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology α]
[topological_space.second_countable_topology β] :
borel_space (α × β)
Equations
theorem
measurable_mul
{α : Type u}
[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}
[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}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_add α]
[has_continuous_add α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), f a + g a)
theorem
measurable.mul
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[has_mul α]
[has_continuous_mul α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), f a * g a)
theorem
measurable_mul_left
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_mul α]
[has_continuous_mul α]
(x : α) :
measurable (λ (y : α), x * y)
theorem
measurable_add_left
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_add α]
[has_continuous_add α]
(x : α) :
measurable (λ (y : α), x + y)
theorem
measurable_mul_right
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_mul α]
[has_continuous_mul α]
(x : α) :
measurable (λ (y : α), y * x)
theorem
measurable_add_right
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[has_add α]
[has_continuous_add α]
(x : α) :
measurable (λ (y : α), y + x)
theorem
finset.measurable_sum
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
{ι : Type u_1}
[add_comm_monoid α]
[has_continuous_add α]
[topological_space.second_countable_topology α]
{f : ι → δ → α}
(s : finset ι) :
(∀ (i : ι), measurable (f i)) → measurable (λ (a : δ), s.sum (λ (i : ι), f i a))
theorem
finset.measurable_prod
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
{ι : Type u_1}
[comm_monoid α]
[has_continuous_mul α]
[topological_space.second_countable_topology α]
{f : ι → δ → α}
(s : finset ι) :
(∀ (i : ι), measurable (f i)) → measurable (λ (a : δ), s.prod (λ (i : ι), f i a))
theorem
measurable_inv
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[group α]
[topological_group α] :
theorem
measurable_neg
{α : Type u}
[topological_space α]
[measurable_space α]
[borel_space α]
[add_group α]
[topological_add_group α] :
theorem
measurable.inv
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[group α]
[topological_group α]
{f : δ → α} :
measurable f → measurable (λ (a : δ), (f a)⁻¹)
theorem
measurable.neg
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
{f : δ → α} :
measurable f → measurable (λ (a : δ), -f a)
theorem
measurable.inv'
{δ : Type x}
[measurable_space δ]
{α : Type u_1}
[normed_field α]
[measurable_space α]
[borel_space α]
{f : δ → α} :
measurable f → measurable (λ (a : δ), (f a)⁻¹)
theorem
measurable.of_neg
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
{f : δ → α} :
measurable (λ (a : δ), -f a) → measurable f
theorem
measurable.of_inv
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[group α]
[topological_group α]
{f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹) → measurable f
@[simp]
theorem
measurable_inv_iff
{α : Type u}
{δ : Type x}
[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}
{δ : Type x}
[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}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[add_group α]
[topological_add_group α]
[topological_space.second_countable_topology α]
{f g : δ → α} :
measurable f → measurable g → measurable (λ (x : δ), f x - g x)
theorem
measurable.is_lub
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
{f : ι → δ → α}
{g : δ → α} :
(∀ (i : ι), measurable (f i)) → (∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) → measurable g
theorem
measurable.is_glb
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
{f : ι → δ → α}
{g : δ → α} :
(∀ (i : ι), measurable (f i)) → (∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) → measurable g
theorem
measurable_supr
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
{f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨆ (i : ι), f i b)
theorem
measurable_infi
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
{f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨅ (i : ι), f i b)
theorem
measurable.supr_Prop
{δ : Type x}
[measurable_space δ]
{α : Type u_1}
[measurable_space α]
[complete_lattice α]
(p : Prop)
{f : δ → α} :
measurable f → measurable (λ (b : δ), ⨆ (h : p), f b)
theorem
measurable.infi_Prop
{δ : Type x}
[measurable_space δ]
{α : Type u_1}
[measurable_space α]
[complete_lattice α]
(p : Prop)
{f : δ → α} :
measurable f → measurable (λ (b : δ), ⨅ (h : p), f b)
theorem
measurable_bsupr
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
(p : ι → Prop)
{f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨆ (i : ι) (hi : p i), f i b)
theorem
measurable_binfi
{α : Type u}
{δ : Type x}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_1}
[encodable ι]
(p : ι → Prop)
{f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨅ (i : ι) (hi : p i), f i b)
def
homemorph.to_measurable_equiv
{α : Type u}
{β : Type v}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β] :
α ≃ₜ β → 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
theorem
is_measurable_ball
{α : Type u}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ} :
is_measurable (metric.ball x ε)
theorem
is_measurable_closed_ball
{α : Type u}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ} :
theorem
measurable_dist
{α : Type u}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), has_dist.dist p.fst p.snd)
theorem
measurable.dist
{α : Type u}
{β : Type v}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α]
[measurable_space β]
{f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), has_dist.dist (f b) (g b))
theorem
measurable_nndist
{α : Type u}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), nndist p.fst p.snd)
theorem
measurable.nndist
{α : Type u}
{β : Type v}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α]
[measurable_space β]
{f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), nndist (f b) (g b))
theorem
is_measurable_eball
{α : Type u}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ennreal} :
is_measurable (emetric.ball x ε)
theorem
measurable_edist
{α : Type u}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
measurable (λ (p : α × α), has_edist.edist p.fst p.snd)
theorem
measurable.edist
{α : Type u}
{β : Type v}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α]
[measurable_space β]
{f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), has_edist.edist (f b) (g b))
theorem
measurable.sub_nnreal
{α : Type u}
[measurable_space α]
{f g : α → nnreal} :
measurable f → measurable g → measurable (λ (a : α), f a - g a)
theorem
measurable.nnreal_of_real
{α : Type u}
[measurable_space α]
{f : α → ℝ} :
measurable f → measurable (λ (x : α), nnreal.of_real (f x))
theorem
measurable.nnreal_coe
{α : Type u}
[measurable_space α]
{f : α → nnreal} :
measurable f → measurable (λ (x : α), ↑(f x))
theorem
measurable.ennreal_coe
{α : Type u}
[measurable_space α]
{f : α → nnreal} :
measurable f → measurable (λ (x : α), ↑(f x))
theorem
measurable.ennreal_of_real
{α : Type u}
[measurable_space α]
{f : α → ℝ} :
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}
[measurable_space α]
{f : ennreal → α} :
measurable (λ (p : nnreal), f ↑p) → measurable f
ennreal is measurable_equiv to nnreal ⊕ unit.
Equations
- ennreal.ennreal_equiv_sum = {to_equiv := {to_fun := (equiv.option_equiv_sum_punit nnreal).to_fun, inv_fun := (equiv.option_equiv_sum_punit nnreal).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_nnreal
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
(f : ennreal → ennreal → β)
{g h : α → ennreal} :
measurable (λ (p : nnreal × nnreal), f ↑(p.fst) ↑(p.snd)) → measurable (λ (r : nnreal), f ⊤ ↑r) → measurable (λ (r : nnreal), f ↑r ⊤) → measurable g → measurable h → measurable (λ (a : α), f (g a) (h a))
theorem
measurable.ennreal_mul
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a * g a)
theorem
measurable.ennreal_add
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a + g a)
theorem
measurable.ennreal_sub
{α : Type u_1}
[measurable_space α]
{f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a - g a)
theorem
measurable_norm
{α : Type u}
[measurable_space α]
[normed_group α]
[opens_measurable_space α] :
theorem
measurable.norm
{α : Type u}
{β : Type v}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α} :
measurable f → measurable (λ (a : β), ∥f a∥)
theorem
measurable_nnnorm
{α : Type u}
[measurable_space α]
[normed_group α]
[opens_measurable_space α] :
theorem
measurable.nnnorm
{α : Type u}
{β : Type v}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α} :
measurable f → measurable (λ (a : β), nnnorm (f a))
theorem
measurable.ennnorm
{α : Type u}
{β : Type v}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α} :
measurable f → measurable (λ (a : β), ↑(nnnorm (f a)))
structure
measure_theory.measure.regular
{α : Type u}
[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}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
⦃A : set α⦄ :
theorem
measure_theory.measure.regular.inner_regular_eq
{α : Type u}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
⦃U : set α⦄ :
theorem
measure_theory.measure.regular.map
{α : Type u}
{β : Type v}
[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}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
{x : ennreal} :