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,ℝ≥0∞.- A measure is
regularif it is finite on compact sets, inner regular and outer regular.
Main statements #
is_open.measurable_set,is_closed.measurable_set: 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;ae_measurable.add: similar dot notation for almost everywhere measurable functions;measurable.ennreal*: special cases for arithmetic operations onℝ≥0∞.
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
topological_space.is_topological_basis.borel_eq_generate_from
{α : Type u_1}
[topological_space α]
[topological_space.second_countable_topology α]
{s : set (set α)}
(hs : topological_space.is_topological_basis s) :
theorem
borel_eq_generate_from_is_closed
{α : Type u_1}
[topological_space α] :
borel α = measurable_space.generate_from {s : set α | is_closed 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_6)
[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.
@[protected, instance]
def
borel_space.opens_measurable
{α : Type u_1}
[topological_space α]
[measurable_space α]
[borel_space α] :
In a borel_space all open sets are measurable.
@[protected, instance]
def
subtype.borel_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[hα : borel_space α]
(s : set α) :
@[protected, instance]
def
subtype.opens_measurable_space
{α : Type u_1}
[topological_space α]
[measurable_space α]
[h : opens_measurable_space α]
(s : set α) :
theorem
is_open.measurable_set
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(h : is_open s) :
theorem
measurable_set_interior
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
theorem
is_Gδ.measurable_set
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(h : is_Gδ s) :
theorem
measurable_set_of_continuous_at
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
{β : Type u_2}
[emetric_space β]
(f : α → β) :
measurable_set {x : α | continuous_at f x}
theorem
is_closed.measurable_set
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(h : is_closed s) :
theorem
is_compact.measurable_set
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t2_space α]
(h : is_compact s) :
theorem
measurable_set_closure
{α : Type u_1}
{s : set α}
[topological_space α]
[measurable_space α]
[opens_measurable_space α] :
theorem
measurable_of_is_open
{γ : Type u_3}
{δ : Type u_5}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_open s → measurable_set (f ⁻¹' s)) :
theorem
measurable_of_is_closed
{γ : Type u_3}
{δ : Type u_5}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_closed s → measurable_set (f ⁻¹' s)) :
theorem
measurable_of_is_closed'
{γ : Type u_3}
{δ : Type u_5}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → γ}
(hf : ∀ (s : set γ), is_closed s → s.nonempty → s ≠ set.univ → measurable_set (f ⁻¹' s)) :
@[protected, instance]
def
nhds_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
(a : α) :
theorem
measurable_set.nhds_within_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
{s : set α}
(hs : measurable_set 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 : measurable_set s.
@[protected, instance]
def
opens_measurable_space.to_measurable_singleton_class
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[t1_space α] :
@[protected, instance]
def
pi.opens_measurable_space
{ι : Type u_1}
{π : ι → Type u_2}
[fintype ι]
[t' : Π (i : ι), topological_space («π» i)]
[Π (i : ι), measurable_space («π» i)]
[∀ (i : ι), topological_space.second_countable_topology («π» i)]
[∀ (i : ι), opens_measurable_space («π» i)] :
opens_measurable_space (Π (i : ι), «π» i)
@[protected, 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 (α × β)
@[simp]
theorem
measurable_set_Ici
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
@[simp]
theorem
measurable_set_Iic
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a : α} :
@[simp]
theorem
measurable_set_Icc
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
measurable_set (set.Icc a b)
@[protected, instance]
def
nhds_within_Ici_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
@[protected, instance]
def
nhds_within_Iic_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α]
{a b : α} :
@[protected, instance]
def
at_top_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
@[protected, instance]
def
at_bot_is_measurably_generated
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[preorder α]
[order_closed_topology α] :
theorem
measurable_set_le'
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[partial_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α] :
measurable_set {p : α × α | p.fst ≤ p.snd}
theorem
measurable_set_le
{α : Type u_1}
{δ : Type u_5}
[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) :
measurable_set {a : δ | f a ≤ g a}
@[simp]
theorem
measurable_set_Iio
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
@[simp]
theorem
measurable_set_Ioi
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a : α} :
@[simp]
theorem
measurable_set_Ioo
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
measurable_set (set.Ioo a b)
@[simp]
theorem
measurable_set_Ioc
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
measurable_set (set.Ioc a b)
@[simp]
theorem
measurable_set_Ico
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
measurable_set (set.Ico a b)
@[protected, 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 : α} :
@[protected, 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
measurable_set_lt'
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α] :
measurable_set {p : α × α | p.fst < p.snd}
theorem
measurable_set_lt
{α : Type u_1}
{δ : Type u_5}
[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) :
measurable_set {a : δ | f a < g a}
theorem
measurable_set_interval
{α : Type u_1}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
measurable_set (set.interval a b)
theorem
measurable.max
{α : Type u_1}
{δ : Type u_5}
[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) :
measurable (λ (a : δ), max (f a) (g a))
theorem
ae_measurable.max
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
{μ : measure_theory.measure δ}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : δ), max (f a) (g a)) μ
theorem
measurable.min
{α : Type u_1}
{δ : Type u_5}
[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) :
measurable (λ (a : δ), min (f a) (g a))
theorem
ae_measurable.min
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space δ]
[linear_order α]
[order_closed_topology α]
[topological_space.second_countable_topology α]
{f g : δ → α}
{μ : measure_theory.measure δ}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_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.
theorem
continuous.ae_measurable
{α : Type u_1}
{γ : Type u_3}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
{f : α → γ}
(h : continuous f)
(μ : measure_theory.measure α) :
ae_measurable f μ
A continuous function from an opens_measurable_space to a borel_space
is ae-measurable.
theorem
closed_embedding.measurable
{α : Type u_1}
{γ : Type u_3}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
{f : α → γ}
(hf : closed_embedding f) :
@[protected, instance]
def
has_continuous_add.has_measurable_add
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[has_add γ]
[has_continuous_add γ] :
@[protected, instance]
def
has_continuous_mul.has_measurable_mul
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[has_mul γ]
[has_continuous_mul γ] :
@[protected, instance]
def
has_continuous_sub.has_measurable_sub
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[has_sub γ]
[has_continuous_sub γ] :
@[protected, instance]
def
topological_add_group.has_measurable_neg
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ] :
@[protected, instance]
def
topological_group.has_measurable_inv
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[group γ]
[topological_group γ] :
@[protected, instance]
def
has_continuous_smul.has_measurable_smul
{M : Type u_1}
{α : Type u_2}
[topological_space M]
[topological_space α]
[measurable_space M]
[measurable_space α]
[opens_measurable_space M]
[borel_space α]
[has_scalar M α]
[has_continuous_smul M α] :
def
homeomorph.to_measurable_equiv
{γ : Type u_3}
{γ₂ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space γ₂]
[measurable_space γ₂]
[borel_space γ₂]
(h : γ ≃ₜ γ₂) :
γ ≃ᵐ γ₂
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 := _}
@[simp]
theorem
homeomorph.to_measurable_equiv_coe
{γ : Type u_3}
{γ₂ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space γ₂]
[measurable_space γ₂]
[borel_space γ₂]
(h : γ ≃ₜ γ₂) :
⇑(h.to_measurable_equiv) = ⇑h
@[simp]
theorem
homeomorph.to_measurable_equiv_symm_coe
{γ : Type u_3}
{γ₂ : Type u_4}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space γ₂]
[measurable_space γ₂]
[borel_space γ₂]
(h : γ ≃ₜ γ₂) :
theorem
homeomorph.measurable
{α : Type u_1}
{γ : Type u_3}
[topological_space α]
[measurable_space α]
[opens_measurable_space α]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
(h : α ≃ₜ γ) :
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 {a}ᶜ) :
theorem
continuous.measurable2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_5}
[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
continuous.ae_measurable2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_5}
[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 : α → β → γ}
{μ : measure_theory.measure δ}
(h : continuous (λ (p : α × β), c p.fst p.snd))
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : δ), c (f a) (g a)) μ
@[protected, instance]
def
has_continuous_inv'.has_measurable_inv
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[group_with_zero γ]
[t1_space γ]
[has_continuous_inv' γ] :
@[protected, instance]
def
has_continuous_mul.has_measurable_mul₂
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[has_mul γ]
[has_continuous_mul γ] :
@[protected, instance]
def
has_continuous_add.has_measurable_mul₂
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[has_add γ]
[has_continuous_add γ] :
@[protected, instance]
def
has_continuous_sub.has_measurable_sub₂
{γ : Type u_3}
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[has_sub γ]
[has_continuous_sub γ] :
@[protected, instance]
def
has_continuous_smul.has_measurable_smul₂
{M : Type u_1}
{α : Type u_2}
[topological_space M]
[topological_space.second_countable_topology M]
[measurable_space M]
[opens_measurable_space M]
[topological_space α]
[topological_space.second_countable_topology α]
[measurable_space α]
[borel_space α]
[has_scalar M α]
[has_continuous_smul M α] :
theorem
pi_le_borel_pi
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space («π» i)]
[Π (i : ι), measurable_space («π» i)]
[∀ (i : ι), borel_space («π» i)] :
measurable_space.pi ≤ borel (Π (i : ι), «π» i)
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 (α × β)
@[protected, instance]
def
pi.borel_space
{ι : Type u_1}
{π : ι → Type u_2}
[fintype ι]
[t' : Π (i : ι), topological_space («π» i)]
[Π (i : ι), measurable_space («π» i)]
[∀ (i : ι), topological_space.second_countable_topology («π» i)]
[∀ (i : ι), borel_space («π» i)] :
borel_space (Π (i : ι), «π» i)
@[protected, 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
closed_embedding.measurable_inv_fun
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[measurable_space β]
[borel_space β]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[n : nonempty β]
{g : β → γ}
(hg : closed_embedding g) :
theorem
measurable_comp_iff_of_closed_embedding
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_5}
[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
ae_measurable_comp_iff_of_closed_embedding
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_5}
[topological_space β]
[measurable_space β]
[borel_space β]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[measurable_space δ]
{f : δ → β}
{μ : measure_theory.measure δ}
(g : β → γ)
(hg : closed_embedding g) :
ae_measurable (g ∘ f) μ ↔ ae_measurable f μ
theorem
ae_measurable_comp_right_iff_of_closed_embedding
{α : Type u_1}
{β : Type u_2}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
[measurable_space δ]
{g : α → β}
{μ : measure_theory.measure α}
{f : β → δ}
(hg : closed_embedding g) :
ae_measurable (f ∘ g) μ ↔ ae_measurable f (⇑(measure_theory.measure.map g) μ)
theorem
measurable_of_Iio
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), measurable_set (f ⁻¹' set.Iio x)) :
theorem
measurable_of_Ioi
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), measurable_set (f ⁻¹' set.Ioi x)) :
theorem
measurable_of_Iic
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), measurable_set (f ⁻¹' set.Iic x)) :
theorem
measurable_of_Ici
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : δ → α}
(hf : ∀ (x : α), measurable_set (f ⁻¹' set.Ici x)) :
theorem
measurable.is_lub
{α : Type u_1}
{δ : Type u_5}
[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
ae_measurable.is_lub
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
[encodable ι]
{f : ι → δ → α}
{g : δ → α}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hg : ∀ᵐ (b : δ) ∂μ, is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :
ae_measurable g μ
theorem
measurable.is_glb
{α : Type u_1}
{δ : Type u_5}
[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
ae_measurable.is_glb
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
[encodable ι]
{f : ι → δ → α}
{g : δ → α}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hg : ∀ᵐ (b : δ) ∂μ, is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :
ae_measurable g μ
theorem
measurable.supr_Prop
{δ : Type u_5}
[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_5}
[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_5}
[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
ae_measurable_supr
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
[encodable ι]
{f : ι → δ → α}
(hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨆ (i : ι), f i b) μ
theorem
measurable_infi
{α : Type u_1}
{δ : Type u_5}
[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
ae_measurable_infi
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
[encodable ι]
{f : ι → δ → α}
(hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨅ (i : ι), f i b) μ
theorem
measurable_bsupr
{α : Type u_1}
{δ : Type u_5}
[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
ae_measurable_bsupr
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
(s : set ι)
{f : ι → δ → α}
(hs : s.countable)
(hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨆ (i : ι) (H : i ∈ s), f i b) μ
theorem
measurable_binfi
{α : Type u_1}
{δ : Type u_5}
[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
ae_measurable_binfi
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{μ : measure_theory.measure δ}
(s : set ι)
{f : ι → δ → α}
(hs : s.countable)
(hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨅ (i : ι) (H : i ∈ s), f i b) μ
theorem
measurable_liminf'
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{ι' : Type u_3}
{f : ι → δ → α}
{u : filter ι}
(hf : ∀ (i : ι), measurable (f i))
{p : ι' → Prop}
{s : ι' → set ι}
(hu : u.has_countable_basis p s)
(hs : ∀ (i : ι'), (s i).countable) :
measurable (λ (x : δ), u.liminf (λ (i : ι), f i x))
liminf over a general filter is measurable. See measurable_liminf for the version over ℕ.
theorem
measurable_limsup'
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{ι : Type u_2}
{ι' : Type u_3}
{f : ι → δ → α}
{u : filter ι}
(hf : ∀ (i : ι), measurable (f i))
{p : ι' → Prop}
{s : ι' → set ι}
(hu : u.has_countable_basis p s)
(hs : ∀ (i : ι'), (s i).countable) :
measurable (λ (x : δ), u.limsup (λ (i : ι), f i x))
limsup over a general filter is measurable. See measurable_limsup for the version over ℕ.
theorem
measurable_liminf
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : ℕ → δ → α}
(hf : ∀ (i : ℕ), measurable (f i)) :
measurable (λ (x : δ), filter.at_top.liminf (λ (i : ℕ), f i x))
liminf over ℕ is measurable. See measurable_liminf' for a version with a general filter.
theorem
measurable_limsup
{α : Type u_1}
{δ : Type u_5}
[topological_space α]
[measurable_space α]
[borel_space α]
[measurable_space δ]
[complete_linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{f : ℕ → δ → α}
(hf : ∀ (i : ℕ), measurable (f i)) :
measurable (λ (x : δ), filter.at_top.limsup (λ (i : ℕ), f i x))
limsup over ℕ is measurable. See measurable_limsup' for a version with a general filter.
theorem
measurable_cSup
{α : Type u_1}
{δ : Type u_5}
[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 : α ≃ₜ β) :
α ≃ᵐ β
Convert a homeomorph to a measurable_equiv.
Equations
- homemorph.to_measurable_equiv h = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem
measurable_set_ball
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ} :
measurable_set (metric.ball x ε)
theorem
measurable_set_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_inf_nndist
{α : Type u_1}
[metric_space α]
[measurable_space α]
[opens_measurable_space α]
{s : set α} :
measurable (λ (x : α), metric.inf_nndist x s)
theorem
measurable.inf_nndist
{α : 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_nndist (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
measurable_set_eball
{α : Type u_1}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
{x : α}
{ε : ℝ≥0∞} :
measurable_set (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
ae_measurable.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[measurable_space α]
[opens_measurable_space α]
[measurable_space β]
[topological_space.second_countable_topology α]
{f g : β → α}
{μ : measure_theory.measure β}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : β), edist (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
ae_measurable.ennreal_coe
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_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 ℝ≥0∞ numbers is measurable_equiv to ℝ≥0.
theorem
ennreal.measurable_of_measurable_nnreal
{α : Type u_1}
[measurable_space α]
{f : ℝ≥0∞ → α}
(h : measurable (λ (p : ℝ≥0), f ↑p)) :
ℝ≥0∞ is measurable_equiv to ℝ≥0 ⊕ 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 : ℝ≥0∞ × β → γ}
(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 : ℝ≥0∞ × ℝ≥0∞ → β}
(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 : α → ℝ≥0∞}
(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 : α → ℝ≥0∞}
(hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
theorem
ae_measurable.to_real
{α : Type u_1}
[measurable_space α]
{f : α → ℝ≥0∞}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
theorem
measurable.ennreal_tsum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
[encodable ι]
{f : ι → α → ℝ≥0∞}
(h : ∀ (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)
note: ℝ≥0∞ can probably be generalized in a future version of this lemma.
theorem
ae_measurable.ennreal_tsum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
[encodable ι]
{f : ι → α → ℝ≥0∞}
{μ : measure_theory.measure α}
(h : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
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
ae_measurable.norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
{μ : measure_theory.measure β}
(hf : ae_measurable f μ) :
ae_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
ae_measurable.nnnorm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
{μ : measure_theory.measure β}
(hf : ae_measurable f μ) :
ae_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
ae_measurable.ennnorm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
{μ : measure_theory.measure β}
(hf : ae_measurable f μ) :
ae_measurable (λ (a : β), ↑(nnnorm (f a))) μ
theorem
measurable_of_tendsto_nnreal'
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{ι' : Type u_3}
{f : ι → α → ℝ≥0}
{g : α → ℝ≥0}
(u : filter ι)
[u.ne_bot]
(hf : ∀ (i : ι), measurable (f i))
(lim : filter.tendsto f u (𝓝 g))
{p : ι' → Prop}
{s : ι' → set ι}
(hu : u.has_countable_basis p s)
(hs : ∀ (i : ι'), (s i).countable) :
A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable.
The assumption hs can be dropped using filter.is_countably_generated.has_antimono_basis, but we
don't need that case yet.
theorem
measurable_of_tendsto_nnreal
{α : Type u_1}
[measurable_space α]
{f : ℕ → α → ℝ≥0}
{g : α → ℝ≥0}
(hf : ∀ (i : ℕ), measurable (f i))
(lim : filter.tendsto f filter.at_top (𝓝 g)) :
A sequential limit of measurable ℝ≥0 valued functions is measurable.
theorem
measurable_of_tendsto_metric'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[metric_space β]
[borel_space β]
{ι : Type u_3}
{ι' : Type u_4}
{f : ι → α → β}
{g : α → β}
(u : filter ι)
[u.ne_bot]
(hf : ∀ (i : ι), measurable (f i))
(lim : filter.tendsto f u (𝓝 g))
{p : ι' → Prop}
{s : ι' → set ι}
(hu : u.has_countable_basis p s)
(hs : ∀ (i : ι'), (s i).countable) :
A limit (over a general filter) of measurable functions valued in a metric space is measurable.
The assumption hs can be dropped using filter.is_countably_generated.has_antimono_basis, but we
don't need that case yet.
theorem
measurable_of_tendsto_metric
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[metric_space β]
[borel_space β]
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (i : ℕ), measurable (f i))
(lim : filter.tendsto f filter.at_top (𝓝 g)) :
A sequential limit of measurable functions valued in a metric space is measurable.
theorem
ae_measurable_of_tendsto_metric_ae
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[metric_space β]
[borel_space β]
{μ : measure_theory.measure α}
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (n : ℕ), ae_measurable (f n) μ)
(h_ae_tendsto : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
ae_measurable g μ
theorem
measurable_of_tendsto_metric_ae
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[metric_space β]
[borel_space β]
{μ : measure_theory.measure α}
[μ.is_complete]
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (n : ℕ), measurable (f n))
(h_ae_tendsto : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (g x))) :
theorem
measurable_limit_of_tendsto_metric_ae
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[metric_space β]
[borel_space β]
{μ : measure_theory.measure α}
{f : ℕ → α → β}
(hf : ∀ (n : ℕ), ae_measurable (f n) μ)
(h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 l)) :
∃ (f_lim : α → β) (hf_lim_meas : measurable f_lim), ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), f n x) filter.at_top (𝓝 (f_lim x))
@[protected]
theorem
continuous_linear_map.measurable
{𝕜 : Type u_6}
[normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[opens_measurable_space E]
{F : Type u_8}
[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_6}
[normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[opens_measurable_space E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space F]
[borel_space F]
(L : E →L[𝕜] F)
{φ : α → E}
(φ_meas : measurable φ) :
measurable (λ (a : α), ⇑L (φ a))
@[protected, instance]
def
continuous_linear_map.measurable_space
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F] :
measurable_space (E →L[𝕜] F)
Equations
@[protected, instance]
def
continuous_linear_map.borel_space
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F] :
borel_space (E →L[𝕜] F)
theorem
continuous_linear_map.measurable_apply
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space F]
[borel_space F]
(x : E) :
measurable (λ (f : E →L[𝕜] F), ⇑f x)
theorem
continuous_linear_map.measurable_apply'
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space E]
[opens_measurable_space E]
[measurable_space F]
[borel_space F] :
measurable (λ (x : E) (f : E →L[𝕜] F), ⇑f x)
theorem
continuous_linear_map.measurable_coe
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
[measurable_space F]
[borel_space F] :
measurable (λ (f : E →L[𝕜] F) (x : E), ⇑f x)
theorem
measurable.apply_continuous_linear_map
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[borel_space E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
{φ : α → (F →L[𝕜] E)}
(hφ : measurable φ)
(v : F) :
measurable (λ (a : α), ⇑(φ a) v)
theorem
ae_measurable.apply_continuous_linear_map
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[borel_space E]
{F : Type u_8}
[normed_group F]
[normed_space 𝕜 F]
{φ : α → (F →L[𝕜] E)}
{μ : measure_theory.measure α}
(hφ : ae_measurable φ μ)
(v : F) :
ae_measurable (λ (a : α), ⇑(φ a) v) μ
theorem
measurable_smul_const
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
[complete_space 𝕜]
[measurable_space 𝕜]
[borel_space 𝕜]
{E : Type u_7}
[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
theorem
ae_measurable_smul_const
{α : Type u_1}
[measurable_space α]
{𝕜 : Type u_6}
[nondiscrete_normed_field 𝕜]
[complete_space 𝕜]
[measurable_space 𝕜]
[borel_space 𝕜]
{E : Type u_7}
[normed_group E]
[normed_space 𝕜 E]
[measurable_space E]
[borel_space E]
{f : α → 𝕜}
{μ : measure_theory.measure α}
{c : E}
(hc : c ≠ 0) :
ae_measurable (λ (x : α), f x • c) μ ↔ ae_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 α⦄, measurable_set 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 : measurable_set 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.exists_compact_not_null
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular) :
@[protected]
theorem
measure_theory.measure.regular.map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
[opens_measurable_space α]
[measurable_space β]
[topological_space β]
[t2_space β]
[borel_space β]
(hμ : μ.regular)
(f : α ≃ₜ β) :
(⇑(measure_theory.measure.map ⇑f) μ).regular
@[protected]
theorem
measure_theory.measure.regular.smul
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
(hμ : μ.regular)
{x : ℝ≥0∞}
(hx : x < ⊤) :
@[protected]
theorem
measure_theory.measure.regular.sigma_finite
{α : Type u_1}
[measurable_space α]
[topological_space α]
{μ : measure_theory.measure α}
[opens_measurable_space α]
[t2_space α]
[sigma_compact_space α]
(hμ : μ.regular) :
A regular measure in a σ-compact space is σ-finite.
theorem
is_compact.measure_lt_top_of_nhds_within
{α : Type u_1}
[measurable_space α]
[topological_space α]
{s : set α}
{μ : measure_theory.measure α}
(h : is_compact s)
(hμ : ∀ (x : α), x ∈ s → μ.finite_at_filter (𝓝[s] x)) :
theorem
is_compact.measure_lt_top
{α : Type u_1}
[measurable_space α]
[topological_space α]
{s : set α}
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
(h : is_compact s) :