mathlib documentation

measure_theory.ae_eq_fun

Almost everywhere equal functions

Two measurable functions are treated as identical if they are almost everywhere equal. We form the set of equivalence classes under the relation of being almost everywhere equal, which is sometimes known as the L⁰ space.

See l1_space.lean for space.

Notation

Main statements

Implementation notes

Tags

function space, almost everywhere equal, L⁰, ae_eq_fun

def measure_theory.measure.ae_eq_setoid {α : Type u_1} (β : Type u_2) [measurable_space α] [measurable_space β] :

The equivalence relation of being almost everywhere equal

Equations
def measure_theory.ae_eq_fun (α : Type u_1) (β : Type u_2) [measurable_space α] [measurable_space β] :
measure_theory.measure αType (max u_1 u_2)

The space of equivalence classes of measurable functions, where two measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

Equations
def measure_theory.ae_eq_fun.mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α → β) :
measurable f→ₘ[μ] β)

Construct the equivalence class [f] of a measurable function f, based on the equivalence relation of being almost everywhere equal.

Equations
@[instance]

A representative of an ae_eq_fun [f]

Equations
theorem measure_theory.ae_eq_fun.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :

@[simp]
theorem measure_theory.ae_eq_fun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α → β) (hf : measurable f) :

@[simp]
theorem measure_theory.ae_eq_fun.quotient_out'_eq_coe_fn {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :

@[simp]
theorem measure_theory.ae_eq_fun.mk_eq_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f g : α → β} {hf : measurable f} {hg : measurable g} :

@[simp]
theorem measure_theory.ae_eq_fun.mk_coe_fn {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :

@[ext]
theorem measure_theory.ae_eq_fun.ext {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f g : α →ₘ[μ] β} :
f =ᵐ[μ] gf = g

theorem measure_theory.ae_eq_fun.coe_fn_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α → β) (hf : measurable f) :

theorem measure_theory.ae_eq_fun.induction_on {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) {p : →ₘ[μ] β) → Prop} :
(∀ (f : α → β) (hf : measurable f), p (measure_theory.ae_eq_fun.mk f hf))p f

theorem measure_theory.ae_eq_fun.induction_on₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [measurable_space β'] {μ' : measure_theory.measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : →ₘ[μ] β)(α' →ₘ[μ'] β') → Prop} :
(∀ (f : α → β) (hf : measurable f) (f' : α' → β') (hf' : measurable f'), p (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk f' hf'))p f f'

theorem measure_theory.ae_eq_fun.induction_on₃ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [measurable_space β'] {μ' : measure_theory.measure α'} {α'' : Type u_5} {β'' : Type u_6} [measurable_space α''] [measurable_space β''] {μ'' : measure_theory.measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'') {p : →ₘ[μ] β)(α' →ₘ[μ'] β')(α'' →ₘ[μ''] β'') → Prop} :
(∀ (f : α → β) (hf : measurable f) (f' : α' → β') (hf' : measurable f') (f'' : α'' → β'') (hf'' : measurable f''), p (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk f' hf') (measure_theory.ae_eq_fun.mk f'' hf''))p f f' f''

def measure_theory.ae_eq_fun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (g : β → γ) :
measurable g→ₘ[μ] β)→ₘ[μ] γ)

Given a measurable function g : β → γ, and an almost everywhere equal function [f] : α →ₘ β, return the equivalence class of g ∘ f, i.e., the almost everywhere equal function [g ∘ f] : α →ₘ γ.

Equations
@[simp]
theorem measure_theory.ae_eq_fun.comp_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α → β) (hf : measurable f) :

theorem measure_theory.ae_eq_fun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :

theorem measure_theory.ae_eq_fun.coe_fn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :

def measure_theory.ae_eq_fun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} :
→ₘ[μ] β)→ₘ[μ] γ)→ₘ[μ] β × γ)

The class of x ↦ (f x, g x).

Equations
@[simp]
theorem measure_theory.ae_eq_fun.pair_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (f : α → β) (hf : measurable f) (g : α → γ) (hg : measurable g) :

theorem measure_theory.ae_eq_fun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
f.pair g = measure_theory.ae_eq_fun.mk (λ (x : α), (f x, g x)) _

theorem measure_theory.ae_eq_fun.coe_fn_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
(f.pair g) =ᵐ[μ] λ (x : α), (f x, g x)

def measure_theory.ae_eq_fun.comp₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) :
measurable (function.uncurry g)→ₘ[μ] β)→ₘ[μ] γ)→ₘ[μ] δ)

Given a measurable function g : β → γ → δ, and almost everywhere equal functions [f₁] : α →ₘ β and [f₂] : α →ₘ γ, return the equivalence class of the function λa, g (f₁ a) (f₂ a), i.e., the almost everywhere equal function [λa, g (f₁ a) (f₂ a)] : α →ₘ γ

Equations
@[simp]
theorem measure_theory.ae_eq_fun.comp₂_mk_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ : measurable f₁) (hf₂ : measurable f₂) :

theorem measure_theory.ae_eq_fun.comp₂_eq_pair {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :

theorem measure_theory.ae_eq_fun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.mk (λ (a : α), g (f₁ a) (f₂ a)) _

theorem measure_theory.ae_eq_fun.coe_fn_comp₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
(measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂) =ᵐ[μ] λ (a : α), g (f₁ a) (f₂ a)

def measure_theory.ae_eq_fun.to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} :
→ₘ[μ] β)μ.ae.germ β

Interpret f : α →ₘ[μ] β as a germ at μ.ae forgetting that f is measurable.

Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α → β) (hf : measurable f) :

theorem measure_theory.ae_eq_fun.to_germ_eq {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :

theorem measure_theory.ae_eq_fun.comp_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :

theorem measure_theory.ae_eq_fun.comp₂_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μ : measure_theory.measure α} (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :

def measure_theory.ae_eq_fun.lift_pred {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} :
(β → Prop)→ₘ[μ] β) → Prop

Given a predicate p and an equivalence class [f], return true if p holds of f a for almost all a

Equations
def measure_theory.ae_eq_fun.lift_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} :
(β → γ → Prop)→ₘ[μ] β)→ₘ[μ] γ) → Prop

Given a relation r and equivalence class [f] and [g], return true if r holds of (f a, g a) for almost all a

Equations
theorem measure_theory.ae_eq_fun.lift_rel_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf : measurable f} {hg : measurable g} :

theorem measure_theory.ae_eq_fun.lift_rel_iff_coe_fn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
measure_theory.ae_eq_fun.lift_rel r f g ∀ᵐ (a : α) ∂μ, r (f a) (g a)

@[simp]
theorem measure_theory.ae_eq_fun.mk_le_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [preorder β] {f g : α → β} (hf : measurable f) (hg : measurable g) :

@[simp]
theorem measure_theory.ae_eq_fun.coe_fn_le {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [preorder β] {f g : α →ₘ[μ] β} :

def measure_theory.ae_eq_fun.const (α : Type u_1) {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} :
β → →ₘ[μ] β)

The equivalence class of a constant function: [λa:α, b], based on the equivalence relation of being almost everywhere equal

Equations
@[instance]
def measure_theory.ae_eq_fun.has_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_zero β] :
has_zero →ₘ[μ] β)

theorem measure_theory.ae_eq_fun.one_def {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_one β] :

theorem measure_theory.ae_eq_fun.zero_def {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_zero β] :

theorem measure_theory.ae_eq_fun.coe_fn_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_zero β] :
0 =ᵐ[μ] 0

theorem measure_theory.ae_eq_fun.coe_fn_one {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_one β] :
1 =ᵐ[μ] 1

@[simp]
theorem measure_theory.ae_eq_fun.zero_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_zero β] :

@[simp]
theorem measure_theory.ae_eq_fun.one_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [has_one β] :

@[instance]

theorem measure_theory.ae_eq_fun.coe_fn_inv {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} [topological_space γ] [borel_space γ] [group γ] [topological_group γ] (f : α →ₘ[μ] γ) :

@[simp]
theorem measure_theory.ae_eq_fun.mk_sub {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} [topological_space γ] [borel_space γ] [add_group γ] [topological_add_group γ] [topological_space.second_countable_topology γ] (f g : α → γ) (hf : measurable (λ (x : α), f x)) (hg : measurable (λ (x : α), g x)) :

@[instance]
def measure_theory.ae_eq_fun.has_scalar {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ] :
has_scalar 𝕜 →ₘ[μ] γ)

Equations
@[simp]
theorem measure_theory.ae_eq_fun.smul_mk {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ] (c : 𝕜) (f : α → γ) (hf : measurable f) :

theorem measure_theory.ae_eq_fun.coe_fn_smul {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f) =ᵐ[μ] c f

theorem measure_theory.ae_eq_fun.smul_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).to_germ = c f.to_germ

For f : α → ennreal, define ∫ [f] to be ∫ f

Equations
@[simp]
theorem measure_theory.ae_eq_fun.lintegral_mk {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α → ennreal) (hf : measurable f) :

@[simp]

comp_edist [f] [g] a will return `edist (f a) (g a)

Equations
theorem measure_theory.ae_eq_fun.coe_fn_edist {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} [emetric_space γ] [topological_space.second_countable_topology γ] [opens_measurable_space γ] (f g : α →ₘ[μ] γ) :
(f.edist g) =ᵐ[μ] λ (a : α), edist (f a) (g a)

@[instance]

Almost everywhere equal functions form an emetric_space, with the emetric defined as edist f g = ∫⁻ a, edist (f a) (g a).

Equations
theorem measure_theory.ae_eq_fun.edist_add_right {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} [normed_group γ] [topological_space.second_countable_topology γ] [borel_space γ] (f g h : α →ₘ[μ] γ) :
edist (f + h) (g + h) = edist f g

theorem measure_theory.ae_eq_fun.edist_smul {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [normed_group γ] [topological_space.second_countable_topology γ] [normed_space 𝕜 γ] [borel_space γ] (c : 𝕜) (f : α →ₘ[μ] γ) :

Positive part of an ae_eq_fun.

Equations