mathlib3 documentation

meta def tactic.add_borel_instance (α : expr) :

Add instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

meta def tactic.borel_to_refl (α i : expr) :

Given a type α, an assumption i : measurable_space α, and an instance [borel_space α], replace i with borel α.

meta def tactic.borelize (α : expr) :

Given a type α, if there is an assumption [i : measurable_space α], then try to prove [borel_space α] and replace i with borel α. Otherwise, add instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

meta def tactic.interactive.borelize (ts : interactive.parse interactive.types.pexpr_list_or_texpr) :

The behaviour of borelize α depends on the existing assumptions on α.

if α is a topological space with instances [measurable_space α] [borel_space α], then borelize α replaces the former instance by borel α;
otherwise, borelize α adds instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

Finally, borelize [α, β, γ] runs borelize α, borelize β, borelize γ.

def tactic_doc.tactic.borelize :

tactic_doc_entry

The behaviour of borelize α depends on the existing assumptions on α.

if α is a topological space with instances [measurable_space α] [borel_space α], then borelize α replaces the former instance by borel α;
otherwise, borelize α adds instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

Finally, borelize [α, β, γ] runs borelize α, borelize β, borelize γ.

opens_measurable_space αᵒᵈ

@[protected, instance]

def order_dual.opens_measurable_space {α : Type u_1} [topological_space α] [measurable_space α] [h : opens_measurable_space α] :

@[protected, instance]

def order_dual.borel_space {α : Type u_1} [topological_space α] [measurable_space α] [h : borel_space α] :

borel_space αᵒᵈ

@[protected, instance]

def borel_space.opens_measurable {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] :

opens_measurable_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 α) :

borel_space ↥s

opens_measurable_space ↥s

@[protected, instance]

def subtype.opens_measurable_space {α : Type u_1} [topological_space α] [measurable_space α] [h : opens_measurable_space α] (s : set α) :

measurable_space.countably_generated α

@[protected, instance]

def borel_space.countably_generated {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [topological_space.second_countable_topology α] :

theorem measurable_set.induction_on_open {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {C : set α → Prop} (h_open : ∀ (U : set α), is_open U → C U) (h_compl : ∀ (t : set α), measurable_set t → C t → C tᶜ) (h_union : ∀ (f : ℕ → set α), pairwise (disjoint on f) → (∀ (i : ℕ), measurable_set (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)) ⦃t : set α⦄ :

measurable_set t → C t

theorem is_open.measurable_set {α : Type u_1} {s : set α} [topological_space α] [measurable_space α] [opens_measurable_space α] (h : is_open s) :

@[measurability]

theorem measurable_set_interior {α : Type u_1} {s : set α} [topological_space α] [measurable_space α] [opens_measurable_space α] :

measurable_set (interior s)

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) :

@[measurability]

theorem measurable_set_closure {α : Type u_1} {s : set α} [topological_space α] [measurable_space α] [opens_measurable_space α] :

measurable_set (closure s)

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 : α) :

(nhds a).is_measurably_generated

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 : α) :

(nhds_within a s).is_measurably_generated

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 α] :

measurable_singleton_class α

@[protected, instance]

def pi.opens_measurable_space {ι : Type u_1} {π : ι → Type u_2} [countable ι] [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 (α × β)

theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : ⇑μ (frontier s) = 0) :

interior s =ᵐ[μ] s

theorem measure_interior_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : ⇑μ (frontier s) = 0) :

⇑μ (interior s) = ⇑μ s

theorem null_measurable_set_of_null_frontier {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] {s : set α} {μ : measure_theory.measure α} (h : ⇑μ (frontier s) = 0) :

measure_theory.null_measurable_set s μ

theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : ⇑μ (frontier s) = 0) :

closure s =ᵐ[μ] s

theorem measure_closure_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : ⇑μ (frontier s) = 0) :

⇑μ (closure s) = ⇑μ s

@[simp, measurability]

theorem measurable_set_Ici {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [preorder α] [order_closed_topology α] {a : α} :

measurable_set (set.Ici a)

@[simp, measurability]

theorem measurable_set_Iic {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [preorder α] [order_closed_topology α] {a : α} :

measurable_set (set.Iic a)

@[simp, measurability]

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 : α} :

(nhds_within a (set.Ici b)).is_measurably_generated

@[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 : α} :

(nhds_within a (set.Iic b)).is_measurably_generated

@[protected, instance]

def nhds_within_Icc_is_measurably_generated {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [preorder α] [order_closed_topology α] {a b x : α} :

(nhds_within x (set.Icc a b)).is_measurably_generated

filter.at_top.is_measurably_generated

@[protected, instance]

def at_top_is_measurably_generated {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [preorder α] [order_closed_topology α] :

filter.at_bot.is_measurably_generated

@[protected, instance]

def at_bot_is_measurably_generated {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [preorder α] [order_closed_topology α] :

@[measurability]

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}

@[measurability]

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, measurability]

theorem measurable_set_Iio {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] {a : α} :

measurable_set (set.Iio a)

@[simp, measurability]

theorem measurable_set_Ioi {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] {a : α} :

measurable_set (set.Ioi a)

@[simp, measurability]

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, measurability]

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, measurability]

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 : α} :

(nhds_within a (set.Ioi b)).is_measurably_generated

@[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 : α} :

(nhds_within a (set.Iio b)).is_measurably_generated

@[protected, instance]

def nhds_within_uIcc_is_measurably_generated {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] {a b x : α} :

(nhds_within x (set.uIcc a b)).is_measurably_generated

@[measurability]

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}

@[measurability]

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 null_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 α] {μ : measure_theory.measure δ} {f g : δ → α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :

measure_theory.null_measurable_set {a : δ | f a < g a} μ

theorem set.ord_connected.measurable_set {α : Type u_1} {s : set α} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] (h : s.ord_connected) :

theorem is_preconnected.measurable_set {α : Type u_1} {s : set α} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] (h : is_preconnected s) :

theorem generate_from_Ico_mem_le_borel {α : Type u_1} [topological_space α] [linear_order α] [order_closed_topology α] (s t : set α) :

measurable_space.generate_from {S : set α | ∃ (l : α) (H : l ∈ s) (u : α) (H : u ∈ t) (h : l < u), set.Ico l u = S} ≤ borel α

theorem dense.borel_eq_generate_from_Ico_mem_aux {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (hd : dense s) (hbot : ∀ (x : α), is_bot x → x ∈ s) (hIoo : ∀ (x y : α), x < y → set.Ioo x y = ∅ → y ∈ s) :

borel α = measurable_space.generate_from {S : set α | ∃ (l : α) (H : l ∈ s) (u : α) (H : u ∈ s) (h : l < u), set.Ico l u = S}

theorem dense.borel_eq_generate_from_Ico_mem {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [densely_ordered α] [no_min_order α] {s : set α} (hd : dense s) :

borel α = measurable_space.generate_from {S : set α | ∃ (l : α) (H : l ∈ s) (u : α) (H : u ∈ s) (h : l < u), set.Ico l u = S}

theorem borel_eq_generate_from_Ico (α : Type u_1) [topological_space α] [topological_space.second_countable_topology α] [linear_order α] [order_topology α] :

borel α = measurable_space.generate_from {S : set α | ∃ (l u : α) (h : l < u), set.Ico l u = S}

theorem dense.borel_eq_generate_from_Ioc_mem_aux {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (hd : dense s) (hbot : ∀ (x : α), is_top x → x ∈ s) (hIoo : ∀ (x y : α), x < y → set.Ioo x y = ∅ → x ∈ s) :

borel α = measurable_space.generate_from {S : set α | ∃ (l : α) (H : l ∈ s) (u : α) (H : u ∈ s) (h : l < u), set.Ioc l u = S}

theorem dense.borel_eq_generate_from_Ioc_mem {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [densely_ordered α] [no_max_order α] {s : set α} (hd : dense s) :

borel α = measurable_space.generate_from {S : set α | ∃ (l : α) (H : l ∈ s) (u : α) (H : u ∈ s) (h : l < u), set.Ioc l u = S}

theorem borel_eq_generate_from_Ioc (α : Type u_1) [topological_space α] [topological_space.second_countable_topology α] [linear_order α] [order_topology α] :

borel α = measurable_space.generate_from {S : set α | ∃ (l u : α) (h : l < u), set.Ioc l u = S}

theorem measure_theory.measure.ext_of_Ico_finite {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] (hμν : ⇑μ set.univ = ⇑ν set.univ) (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ico a b) = ⇑ν (set.Ico a b)) :

μ = ν

Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If α is a conditionally complete linear order with no top element, measure_theory.measure..ext_of_Ico is an extensionality lemma with weaker assumptions on μ and ν.

theorem measure_theory.measure.ext_of_Ioc_finite {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] (hμν : ⇑μ set.univ = ⇑ν set.univ) (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ioc a b) = ⇑ν (set.Ioc a b)) :

μ = ν

Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If α is a conditionally complete linear order with no top element, measure_theory.measure..ext_of_Ioc is an extensionality lemma with weaker assumptions on μ and ν.

theorem measure_theory.measure.ext_of_Ico' {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] [no_max_order α] (μ ν : measure_theory.measure α) (hμ : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ico a b) ≠ ⊤) (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ico a b) = ⇑ν (set.Ico a b)) :

μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

theorem measure_theory.measure.ext_of_Ioc' {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] [no_min_order α] (μ ν : measure_theory.measure α) (hμ : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ioc a b) ≠ ⊤) (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ioc a b) = ⇑ν (set.Ioc a b)) :

μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

theorem measure_theory.measure.ext_of_Ico {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [conditionally_complete_linear_order α] [order_topology α] [borel_space α] [no_max_order α] (μ ν : measure_theory.measure α) [measure_theory.is_locally_finite_measure μ] (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ico a b) = ⇑ν (set.Ico a b)) :

μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

theorem measure_theory.measure.ext_of_Ioc {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [conditionally_complete_linear_order α] [order_topology α] [borel_space α] [no_min_order α] (μ ν : measure_theory.measure α) [measure_theory.is_locally_finite_measure μ] (h : ∀ ⦃a b : α⦄, a < b → ⇑μ (set.Ioc a b) = ⇑ν (set.Ioc a b)) :

μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

theorem measure_theory.measure.ext_of_Iic {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] (h : ∀ (a : α), ⇑μ (set.Iic a) = ⇑ν (set.Iic a)) :

μ = ν

Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

theorem measure_theory.measure.ext_of_Ici {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] (μ ν : measure_theory.measure α) [measure_theory.is_finite_measure μ] (h : ∀ (a : α), ⇑μ (set.Ici a) = ⇑ν (set.Ici a)) :

μ = ν

Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

@[measurability]

theorem measurable_set_uIcc {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] {a b : α} :

measurable_set (set.uIcc a b)

@[measurability]

theorem measurable_set_uIoc {α : Type u_1} [topological_space α] [measurable_space α] [opens_measurable_space α] [linear_order α] [order_closed_topology α] {a b : α} :

measurable_set (set.uIoc a b)

@[measurability]

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 : δ), linear_order.max (f a) (g a))

@[measurability]

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 : δ), linear_order.max (f a) (g a)) μ

@[measurability]

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 : δ), linear_order.min (f a) (g a))

@[measurability]

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 : δ), linear_order.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) :

theorem continuous.is_open_pos_measure_map {β : Type u_2} {γ : Type u_3} [topological_space β] [measurable_space β] [opens_measurable_space β] [topological_space γ] [measurable_space γ] [borel_space γ] {f : β → γ} (hf : continuous f) (hf_surj : function.surjective f) {μ : measure_theory.measure β} [μ.is_open_pos_measure] :

(measure_theory.measure.map f μ).is_open_pos_measure

theorem continuous_on.measurable_piecewise {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] {f g : α → γ} {s : set α} [Π (j : α), decidable (j ∈ s)] (hf : continuous_on f s) (hg : continuous_on g sᶜ) (hs : measurable_set s) :

measurable (s.piecewise f g)

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

@[protected, instance]

def has_continuous_add.has_measurable_add {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [has_add γ] [has_continuous_add γ] :

has_measurable_add γ

@[protected, instance]

def has_continuous_mul.has_measurable_mul {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [has_mul γ] [has_continuous_mul γ] :

has_measurable_mul γ

@[protected, instance]

def has_continuous_sub.has_measurable_sub {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [has_sub γ] [has_continuous_sub γ] :

has_measurable_sub γ

@[protected, instance]

def topological_add_group.has_measurable_neg {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [add_group γ] [topological_add_group γ] :

has_measurable_neg γ

@[protected, instance]

def topological_group.has_measurable_inv {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [group γ] [topological_group γ] :

has_measurable_inv γ

@[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_smul M α] [has_continuous_smul M α] :

has_measurable_smul M α

@[protected, instance]

def has_continuous_sup.has_measurable_sup {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [has_sup γ] [has_continuous_sup γ] :

has_measurable_sup γ

@[protected, instance]

def has_continuous_sup.has_measurable_sup₂ {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [topological_space.second_countable_topology γ] [has_sup γ] [has_continuous_sup γ] :

has_measurable_sup₂ γ

@[protected, instance]

def has_continuous_inf.has_measurable_inf {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [has_inf γ] [has_continuous_inf γ] :

has_measurable_inf γ

@[protected, instance]

def has_continuous_inf.has_measurable_inf₂ {γ : Type u_3} [topological_space γ] [measurable_space γ] [borel_space γ] [topological_space.second_countable_topology γ] [has_inf γ] [has_continuous_inf γ] :

has_measurable_inf₂ γ

@[protected, measurability]

theorem homeomorph.measurable {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] (h : α ≃ₜ γ) :

measurable ⇑h

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 : γ ≃ₜ γ₂) :

⇑(h.to_measurable_equiv.symm) = ⇑(h.symm)

@[measurability]

theorem continuous_map.measurable {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] (f : C(α, γ)) :

measurable ⇑f

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₀ γ] :

has_measurable_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 γ] :

has_measurable_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 γ] :

has_measurable_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 γ] :

has_measurable_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_smul M α] [has_continuous_smul M α] :

has_measurable_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} [countable ι] [Π (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 (α × β)

@[protected]

theorem embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] {f : α → β} (h₁ : embedding f) (h₂ : measurable_set (set.range f)) :

measurable_embedding f

@[protected]

theorem closed_embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] {f : α → β} (h : closed_embedding f) :

measurable_embedding f

@[protected]

theorem open_embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] {f : α → β} (h : open_embedding f) :

measurable_embedding f

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 upper_semicontinuous.measurable {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [topological_space δ] [opens_measurable_space δ] {f : δ → α} (hf : upper_semicontinuous f) :

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 lower_semicontinuous.measurable {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [topological_space δ] [opens_measurable_space δ] {f : δ → α} (hf : lower_semicontinuous f) :

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 α] {ι : Sort u_2} [countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), measurable (f i)) (hg : ∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :

measurable g

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 α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {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 α] {ι : Sort u_2} [countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), measurable (f i)) (hg : ∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :

measurable g

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 α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :

ae_measurable g μ

@[protected]

theorem monotone.measurable {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [linear_order β] [order_closed_topology β] {f : β → α} (hf : monotone f) :

theorem ae_measurable_restrict_of_monotone_on {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [linear_order β] [order_closed_topology β] {μ : measure_theory.measure β} {s : set β} (hs : measurable_set s) {f : β → α} (hf : monotone_on f s) :

ae_measurable f (μ.restrict s)

@[protected]

theorem antitone.measurable {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [linear_order β] [order_closed_topology β] {f : β → α} (hf : antitone f) :

theorem ae_measurable_restrict_of_antitone_on {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [linear_order β] [order_closed_topology β] {μ : measure_theory.measure β} {s : set β} (hs : measurable_set s) {f : β → α} (hf : antitone_on f s) :

ae_measurable f (μ.restrict s)

theorem measurable_set_of_mem_nhds_within_Ioi_aux {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (h : ∀ (x : α), x ∈ s → s ∈ nhds_within x (set.Ioi x)) (h' : ∀ (x : α), x ∈ s → (∃ (y : α), x < y)) :

theorem measurable_set_of_mem_nhds_within_Ioi {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (h : ∀ (x : α), x ∈ s → s ∈ nhds_within x (set.Ioi x)) :

If a set is a right-neighborhood of all of its points, then it is measurable.

@[measurability]

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)

@[measurability]

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)

@[measurability]

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 α] {ι : Sort u_2} [countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) :

measurable (λ (b : δ), ⨆ (i : ι), f i b)

@[measurability]

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 α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) :

ae_measurable (λ (b : δ), ⨆ (i : ι), f i b) μ

@[measurability]

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 α] {ι : Sort u_2} [countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) :

measurable (λ (b : δ), ⨅ (i : ι), f i b)

@[measurability]

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 α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {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 : δ), filter.liminf (λ (i : ι), f i x) u)

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 : δ), filter.limsup (λ (i : ι), f i x) u)

limsup over a general filter is measurable. See measurable_limsup for the version over ℕ.

@[measurability]

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.liminf (λ (i : ℕ), f i x) filter.at_top)

liminf over ℕ is measurable. See measurable_liminf' for a version with a general filter.

@[measurability]

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.limsup (λ (i : ℕ), f i x) filter.at_top)

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 α] [order_topology α] [topological_space.second_countable_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 : δ), has_Sup.Sup ((λ (i : ι), f i x) '' s))

theorem measurable_cInf {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} {f : ι → δ → α} {s : set ι} (hs : s.countable) (hf : ∀ (i : ι), measurable (f i)) (bdd : ∀ (x : δ), bdd_below ((λ (i : ι), f i x) '' s)) :

measurable (λ (x : δ), has_Inf.Inf ((λ (i : ι), f i x) '' s))

theorem measurable_csupr {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) (bdd : ∀ (x : δ), bdd_above (set.range (λ (i : ι), f i x))) :

measurable (λ (x : δ), ⨆ (i : ι), f i x)

theorem measurable_cinfi {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) (bdd : ∀ (x : δ), bdd_below (set.range (λ (i : ι), f i x))) :

measurable (λ (x : δ), ⨅ (i : ι), f i x)

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 := _}

measure_theory.is_finite_measure_on_compacts (measure_theory.measure.map ⇑f μ)

@[protected]

theorem is_finite_measure_on_compacts.map {α : Type u_1} {m0 : measurable_space α} [topological_space α] [opens_measurable_space α] {β : Type u_2} [measurable_space β] [topological_space β] [borel_space β] [t2_space β] (μ : measure_theory.measure α) [measure_theory.is_finite_measure_on_compacts μ] (f : α ≃ₜ β) :

@[protected, instance]

def empty.borel_space :

borel_space empty

@[protected, instance]

def unit.borel_space :

borel_space unit

@[protected, instance]

def bool.borel_space :

borel_space bool

@[protected, instance]

def nat.borel_space :

borel_space ℕ

@[protected, instance]

def int.borel_space :

borel_space ℤ

@[protected, instance]

def rat.borel_space :

borel_space ℚ

@[protected, instance]

def real.measurable_space :

measurable_space ℝ

Equations

real.measurable_space = borel ℝ

@[protected, instance]

def real.borel_space :

borel_space ℝ

@[protected, instance]

def nnreal.measurable_space :

measurable_space nnreal

Equations

nnreal.measurable_space = subtype.measurable_space

@[protected, instance]

def nnreal.borel_space :

borel_space nnreal

@[protected, instance]

noncomputable def ennreal.measurable_space :

measurable_space ennreal

Equations

ennreal.measurable_space = borel ennreal

@[protected, instance]

def ennreal.borel_space :

borel_space ennreal

@[protected, instance]

noncomputable def ereal.measurable_space :

measurable_space ereal

Equations

ereal.measurable_space = borel ereal

@[protected, instance]

def ereal.borel_space :

borel_space ereal

theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) {f : α → ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) {t : nnreal} (ht : 1 < t) :

⇑μ s = ⇑μ (s ∩ f ⁻¹' {0}) + ⇑μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), ⇑μ (s ∩ f ⁻¹' set.Ico (↑t ^ n) (↑t ^ (n + 1)))

One can cut out ℝ≥0∞ into the sets {0}, Ico (t^n) (t^(n+1)) for n : ℤ and {∞}. This gives a way to compute the measure of a set in terms of sets on which a given function f does not fluctuate by more than t.

@[measurability]

theorem measurable_set_ball {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : ℝ} :

measurable_set (metric.ball x ε)

@[measurability]

theorem measurable_set_closed_ball {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : ℝ} :

measurable_set (metric.closed_ball x ε)

@[measurability]

theorem measurable_inf_dist {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :

measurable (λ (x : α), metric.inf_dist x s)

@[measurability]

theorem measurable.inf_dist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :

measurable (λ (x : β), metric.inf_dist (f x) s)

@[measurability]

theorem measurable_inf_nndist {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :

measurable (λ (x : α), metric.inf_nndist x s)

@[measurability]

theorem measurable.inf_nndist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :

measurable (λ (x : β), metric.inf_nndist (f x) s)

@[measurability]

theorem measurable_dist {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [topological_space.second_countable_topology α] :

measurable (λ (p : α × α), has_dist.dist p.fst p.snd)

@[measurability]

theorem measurable.dist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} (hf : measurable f) (hg : measurable g) :

measurable (λ (b : β), has_dist.dist (f b) (g b))

@[measurability]

theorem measurable_nndist {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [topological_space.second_countable_topology α] :

measurable (λ (p : α × α), has_nndist.nndist p.fst p.snd)

@[measurability]

theorem measurable.nndist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} (hf : measurable f) (hg : measurable g) :

measurable (λ (b : β), has_nndist.nndist (f b) (g b))

theorem tendsto_measure_cthickening {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} (hs : ∃ (R : ℝ) (H : R > 0), ⇑μ (metric.cthickening R s) ≠ ⊤) :

filter.tendsto (λ (r : ℝ), ⇑μ (metric.cthickening r s)) (nhds 0) (nhds (⇑μ (closure s)))

If a set has a closed thickening with finite measure, then the measure of its r-closed thickenings converges to the measure of its closure as r tends to 0.

theorem tendsto_measure_cthickening_of_is_closed {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} (hs : ∃ (R : ℝ) (H : R > 0), ⇑μ (metric.cthickening R s) ≠ ⊤) (h's : is_closed s) :

filter.tendsto (λ (r : ℝ), ⇑μ (metric.cthickening r s)) (nhds 0) (nhds (⇑μ s))

If a closed set has a closed thickening with finite measure, then the measure of its r-closed thickenings converges to its measure as r tends to 0.

theorem tendsto_measure_cthickening_of_is_compact {α : Type u_1} [metric_space α] [measurable_space α] [opens_measurable_space α] [proper_space α] {μ : measure_theory.measure α} [measure_theory.is_finite_measure_on_compacts μ] {s : set α} (hs : is_compact s) :

filter.tendsto (λ (r : ℝ), ⇑μ (metric.cthickening r s)) (nhds 0) (nhds (⇑μ s))

Given a compact set in a proper space, the measure of its r-closed thickenings converges to its measure as r tends to 0.

@[measurability]

theorem measurable_set_eball {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : ennreal} :

measurable_set (emetric.ball x ε)

@[measurability]

theorem measurable_edist_right {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} :

measurable (has_edist.edist x)

@[measurability]

theorem measurable_edist_left {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} :

measurable (λ (y : α), has_edist.edist y x)

@[measurability]

theorem measurable_inf_edist {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :

measurable (λ (x : α), emetric.inf_edist x s)

@[measurability]

theorem measurable.inf_edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :

measurable (λ (x : β), emetric.inf_edist (f x) s)

@[measurability]

theorem measurable_edist {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [topological_space.second_countable_topology α] :

measurable (λ (p : α × α), has_edist.edist p.fst p.snd)

@[measurability]

theorem measurable.edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} (hf : measurable f) (hg : measurable g) :

measurable (λ (b : β), has_edist.edist (f b) (g b))

@[measurability]

theorem ae_measurable.edist {α : Type u_1} {β : Type u_2} [pseudo_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 : β), has_edist.edist (f a) (g a)) μ

theorem real.borel_eq_generate_from_Ioo_rat :

borel ℝ = measurable_space.generate_from (⋃ (a b : ℚ) (h : a < b), {set.Ioo ↑a ↑b})

theorem real.is_pi_system_Ioo_rat :

is_pi_system (⋃ (a b : ℚ) (h : a < b), {set.Ioo ↑a ↑b})

def real.finite_spanning_sets_in_Ioo_rat (μ : measure_theory.measure ℝ) [measure_theory.is_locally_finite_measure μ] :

μ.finite_spanning_sets_in (⋃ (a b : ℚ) (h : a < b), {set.Ioo ↑a ↑b})

The intervals (-(n + 1), (n + 1)) form a finite spanning sets in the set of open intervals with rational endpoints for a locally finite measure μ on ℝ.

Equations

real.finite_spanning_sets_in_Ioo_rat μ = {set := λ (n : ℕ), set.Ioo (-(↑n + 1)) (↑n + 1), set_mem := real.finite_spanning_sets_in_Ioo_rat._proof_1, finite := _, spanning := real.finite_spanning_sets_in_Ioo_rat._proof_3}

theorem real.measure_ext_Ioo_rat {μ ν : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (h : ∀ (a b : ℚ), ⇑μ (set.Ioo ↑a ↑b) = ⇑ν (set.Ioo ↑a ↑b)) :

μ = ν

theorem real.borel_eq_generate_from_Iio_rat :

borel ℝ = measurable_space.generate_from (⋃ (a : ℚ), {set.Iio ↑a})

measurable real.to_nnreal

@[measurability]

theorem measurable_real_to_nnreal :

@[measurability]

theorem measurable.real_to_nnreal {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), (f x).to_nnreal)

@[measurability]

theorem ae_measurable.real_to_nnreal {α : Type u_1} [measurable_space α] {f : α → ℝ} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), (f x).to_nnreal) μ

@[measurability]

theorem measurable_coe_nnreal_real :

@[measurability]

theorem measurable.coe_nnreal_real {α : Type u_1} [measurable_space α] {f : α → nnreal} (hf : measurable f) :

measurable (λ (x : α), ↑(f x))

@[measurability]

theorem ae_measurable.coe_nnreal_real {α : Type u_1} [measurable_space α] {f : α → nnreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), ↑(f x)) μ

@[measurability]

theorem measurable_coe_nnreal_ennreal :

@[measurability]

theorem measurable.coe_nnreal_ennreal {α : Type u_1} [measurable_space α] {f : α → nnreal} (hf : measurable f) :

measurable (λ (x : α), ↑(f x))

@[measurability]

theorem ae_measurable.coe_nnreal_ennreal {α : Type u_1} [measurable_space α] {f : α → nnreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), ↑(f x)) μ

@[measurability]

theorem measurable.ennreal_of_real {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), ennreal.of_real (f x))

@[simp, norm_cast]

theorem measurable_coe_nnreal_real_iff {α : Type u_1} [measurable_space α] {f : α → nnreal} :

measurable (λ (x : α), ↑(f x)) ↔ measurable f

@[simp, norm_cast]

theorem ae_measurable_coe_nnreal_real_iff {α : Type u_1} [measurable_space α] {f : α → nnreal} {μ : measure_theory.measure α} :

ae_measurable (λ (x : α), ↑(f x)) μ ↔ ae_measurable f μ

noncomputable def measurable_equiv.ennreal_equiv_nnreal :

↥{r : ennreal | r ≠ ⊤} ≃ᵐ nnreal

The set of finite ℝ≥0∞ numbers is measurable_equiv to ℝ≥0.

Equations

measurable_equiv.ennreal_equiv_nnreal = ennreal.ne_top_homeomorph_nnreal.to_measurable_equiv

theorem ennreal.measurable_of_measurable_nnreal {α : Type u_1} [measurable_space α] {f : ennreal → α} (h : measurable (λ (p : nnreal), f ↑p)) :

def ennreal.ennreal_equiv_sum :

ennreal ≃ᵐ nnreal ⊕ unit

ℝ≥0∞ is measurable_equiv to ℝ≥0 ⊕ 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_prod {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] {f : ennreal × β → γ} (H₁ : measurable (λ (p : nnreal × β), 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 : nnreal × nnreal), f (↑(p.fst), ↑(p.snd)))) (h₂ : measurable (λ (r : nnreal), f (⊤, ↑r))) (h₃ : measurable (λ (r : nnreal), f (↑r, ⊤))) :

measurable ennreal.of_real

@[measurability]

theorem ennreal.measurable_of_real :

measurable ennreal.to_real

@[measurability]

theorem ennreal.measurable_to_real :

measurable ennreal.to_nnreal

@[measurability]

theorem ennreal.measurable_to_nnreal :

has_measurable_mul₂ ennreal

@[protected, instance]

def ennreal.has_measurable_mul₂ :

has_measurable_sub₂ ennreal

@[protected, instance]

def ennreal.has_measurable_sub₂ :

has_measurable_inv ennreal

@[protected, instance]

def ennreal.has_measurable_inv :

@[measurability]

theorem measurable.ennreal_to_nnreal {α : Type u_1} [measurable_space α] {f : α → ennreal} (hf : measurable f) :

measurable (λ (x : α), (f x).to_nnreal)

@[measurability]

theorem ae_measurable.ennreal_to_nnreal {α : Type u_1} [measurable_space α] {f : α → ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), (f x).to_nnreal) μ

@[simp, norm_cast]

theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} [measurable_space α] {f : α → nnreal} :

measurable (λ (x : α), ↑(f x)) ↔ measurable f

@[simp, norm_cast]

theorem ae_measurable_coe_nnreal_ennreal_iff {α : Type u_1} [measurable_space α] {f : α → nnreal} {μ : measure_theory.measure α} :

ae_measurable (λ (x : α), ↑(f x)) μ ↔ ae_measurable f μ

@[measurability]

theorem measurable.ennreal_to_real {α : Type u_1} [measurable_space α] {f : α → ennreal} (hf : measurable f) :

measurable (λ (x : α), (f x).to_real)

@[measurability]

theorem ae_measurable.ennreal_to_real {α : Type u_1} [measurable_space α] {f : α → ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), (f x).to_real) μ

@[measurability]

theorem measurable.ennreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι → α → ennreal} (h : ∀ (i : ι), measurable (f i)) :

measurable (λ (x : α), ∑' (i : ι), f i x)

note: ℝ≥0∞ can probably be generalized in a future version of this lemma.

@[measurability]

theorem measurable.ennreal_tsum' {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι → α → ennreal} (h : ∀ (i : ι), measurable (f i)) :

measurable (∑' (i : ι), f i)

@[measurability]

theorem measurable.nnreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι → α → nnreal} (h : ∀ (i : ι), measurable (f i)) :

measurable (λ (x : α), ∑' (i : ι), f i x)

@[measurability]

theorem ae_measurable.ennreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι → α → ennreal} {μ : measure_theory.measure α} (h : ∀ (i : ι), ae_measurable (f i) μ) :

ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ

@[measurability]

theorem ae_measurable.nnreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι → α → nnreal} {μ : measure_theory.measure α} (h : ∀ (i : ι), ae_measurable (f i) μ) :

ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ

@[measurability]

theorem measurable_coe_real_ereal :

@[measurability]

theorem measurable.coe_real_ereal {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), ↑(f x))

@[measurability]

theorem ae_measurable.coe_real_ereal {α : Type u_1} [measurable_space α] {f : α → ℝ} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), ↑(f x)) μ

noncomputable def measurable_equiv.ereal_equiv_real :

↥{⊥, ⊤}ᶜ ≃ᵐ ℝ

The set of finite ereal numbers is measurable_equiv to ℝ.

Equations

measurable_equiv.ereal_equiv_real = ereal.ne_bot_top_homeomorph_real.to_measurable_equiv

theorem ereal.measurable_of_measurable_real {α : Type u_1} [measurable_space α] {f : ereal → α} (h : measurable (λ (p : ℝ), f ↑p)) :

@[measurability]

theorem measurable_ereal_to_real :

measurable ereal.to_real

@[measurability]

theorem measurable.ereal_to_real {α : Type u_1} [measurable_space α] {f : α → ereal} (hf : measurable f) :

measurable (λ (x : α), (f x).to_real)

@[measurability]

theorem ae_measurable.ereal_to_real {α : Type u_1} [measurable_space α] {f : α → ereal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), (f x).to_real) μ

@[measurability]

theorem measurable_coe_ennreal_ereal :

@[measurability]

theorem measurable.coe_ereal_ennreal {α : Type u_1} [measurable_space α] {f : α → ennreal} (hf : measurable f) :

measurable (λ (x : α), ↑(f x))

@[measurability]

theorem ae_measurable.coe_ereal_ennreal {α : Type u_1} [measurable_space α] {f : α → ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :

ae_measurable (λ (x : α), ↑(f x)) μ

@[measurability]

theorem measurable_norm {α : Type u_1} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] :

measurable has_norm.norm

@[measurability]

theorem measurable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) :

measurable (λ (a : β), ‖f a‖)

@[measurability]

theorem ae_measurable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) :

ae_measurable (λ (a : β), ‖f a‖) μ

measurable has_nnnorm.nnnorm

@[measurability]

theorem measurable_nnnorm {α : Type u_1} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] :

@[measurability]

theorem measurable.nnnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) :

measurable (λ (a : β), ‖f a‖₊)

@[measurability]

theorem ae_measurable.nnnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) :

ae_measurable (λ (a : β), ‖f a‖₊) μ

@[measurability]

theorem measurable_ennnorm {α : Type u_1} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] :

measurable (λ (x : α), ↑‖x‖₊)

@[measurability]

theorem measurable.ennnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) :

measurable (λ (a : β), ↑‖f a‖₊)