mathlib documentation

measure_theory.function.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 β] (μ : measure_theory.measure α) :
setoid {f // ae_measurable f μ}

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 α] {μ : measure_theory.measure α} [measurable_space β] (f : α → β) (hf : ae_measurable f μ) :
α →ₘ[μ] β

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

Equations
@[instance]
def measure_theory.ae_eq_fun.has_coe_to_fun {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] :
has_coe_to_fun →ₘ[μ] β) (λ (_x : α →ₘ[μ] β), α → β)

A measurable representative of an ae_eq_fun [f]

Equations
theorem measure_theory.ae_eq_fun.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) :
theorem measure_theory.ae_eq_fun.ae_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) :
@[simp]
theorem measure_theory.ae_eq_fun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α → β) (hf : ae_measurable f μ) :
@[simp]
theorem measure_theory.ae_eq_fun.mk_eq_mk {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {f g : α → β} {hf : ae_measurable f μ} {hg : ae_measurable g μ} :
@[simp]
theorem measure_theory.ae_eq_fun.mk_coe_fn {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) :
@[ext]
theorem measure_theory.ae_eq_fun.ext {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {f g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.ae_eq_fun.ext_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {f g : α →ₘ[μ] β} :
f = g f =ᵐ[μ] g
theorem measure_theory.ae_eq_fun.coe_fn_mk {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α → β) (hf : ae_measurable f μ) :
theorem measure_theory.ae_eq_fun.induction_on {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) {p : →ₘ[μ] β) → Prop} (H : ∀ (f : α → β) (hf : ae_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 α] {μ : measure_theory.measure α} [measurable_space β] {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [measurable_space β'] {μ' : measure_theory.measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : →ₘ[μ] β)(α' →ₘ[μ'] β') → Prop} (H : ∀ (f : α → β) (hf : ae_measurable f μ) (f' : α' → β') (hf' : ae_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 α] {μ : measure_theory.measure α} [measurable_space β] {α' : 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} (H : ∀ (f : α → β) (hf : ae_measurable f μ) (f' : α' → β') (hf' : ae_measurable f' μ') (f'' : α'' → β'') (hf'' : ae_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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
α →ₘ[μ] γ

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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α → β) (hf : ae_measurable f μ) :
theorem measure_theory.ae_eq_fun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
def measure_theory.ae_eq_fun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
α →ₘ[μ] β × γ

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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (f : α → β) (hf : ae_measurable f μ) (g : α → γ) (hg : ae_measurable g μ) :
theorem measure_theory.ae_eq_fun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (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 α] {μ : measure_theory.measure α} [measurable_space β] {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
α →ₘ[μ] δ

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 α] {μ : measure_theory.measure α} [measurable_space β] {γ : Type u_3} {δ : Type u_4} [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ : ae_measurable f₁ μ) (hf₂ : ae_measurable f₂ μ) :
theorem measure_theory.ae_eq_fun.comp₂_eq_pair {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {γ : 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 α] {μ : measure_theory.measure α} [measurable_space β] {γ : 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 α] {μ : measure_theory.measure α} [measurable_space β] {γ : 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 α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) :
μ.ae.germ β

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

Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α → β) (hf : ae_measurable f μ) :
theorem measure_theory.ae_eq_fun.to_germ_eq {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (f : α →ₘ[μ] β) :
theorem measure_theory.ae_eq_fun.comp_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] [measurable_space δ] (g : β → γ → δ) (hg : measurable (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
def measure_theory.ae_eq_fun.lift_pred {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (p : β → Prop) (f : α →ₘ[μ] β) :
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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
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 α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf : ae_measurable f μ} {hg : ae_measurable g μ} :
theorem measure_theory.ae_eq_fun.lift_rel_iff_coe_fn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [measurable_space γ] {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 α] {μ : measure_theory.measure α} [measurable_space β] [preorder β] {f g : α → β} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
@[simp]
theorem measure_theory.ae_eq_fun.coe_fn_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [preorder β] {f g : α →ₘ[μ] β} :
def measure_theory.ae_eq_fun.const (α : Type u_1) {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] (b : β) :
α →ₘ[μ] β

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

Equations
theorem measure_theory.ae_eq_fun.coe_fn_zero {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [has_zero β] :
0 =ᵐ[μ] 0
theorem measure_theory.ae_eq_fun.coe_fn_one {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [has_one β] :
1 =ᵐ[μ] 1
@[simp]
theorem measure_theory.ae_eq_fun.zero_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [has_zero β] :
@[simp]
theorem measure_theory.ae_eq_fun.one_to_germ {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] [has_one β] :
@[instance]
Equations
@[instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_inv {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] [topological_space γ] [borel_space γ] [group γ] [topological_group γ] (f : α →ₘ[μ] γ) :
@[simp]
theorem measure_theory.ae_eq_fun.mk_div {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] [topological_space γ] [borel_space γ] [group γ] [topological_group γ] [topological_space.second_countable_topology γ] (f g : α → γ) (hf : ae_measurable (λ (a : α), f a) μ) (hg : ae_measurable (λ (a : α), g a) μ) :
@[simp]
theorem measure_theory.ae_eq_fun.mk_sub {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] [topological_space γ] [borel_space γ] [add_group γ] [topological_add_group γ] [topological_space.second_countable_topology γ] (f g : α → γ) (hf : ae_measurable (λ (a : α), f a) μ) (hg : ae_measurable (λ (a : α), g a) μ) :
@[instance]
def measure_theory.ae_eq_fun.has_scalar {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [module 𝕜 γ] [has_continuous_smul 𝕜 γ] :
has_scalar 𝕜 →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.smul_mk {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [module 𝕜 γ] [has_continuous_smul 𝕜 γ] (c : 𝕜) (f : α → γ) (hf : ae_measurable f μ) :
theorem measure_theory.ae_eq_fun.coe_fn_smul {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [module 𝕜 γ] [has_continuous_smul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f) =ᵐ[μ] c f
theorem measure_theory.ae_eq_fun.smul_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [measurable_space γ] {𝕜 : Type u_5} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [topological_space γ] [borel_space γ] [add_comm_monoid γ] [module 𝕜 γ] [has_continuous_smul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).to_germ = c f.to_germ

For f : α → ℝ≥0∞, define ∫ [f] to be ∫ f

Equations
@[simp]
theorem measure_theory.ae_eq_fun.lintegral_mk {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α → ℝ≥0∞) (hf : ae_measurable f μ) :

Positive part of an ae_eq_fun.

Equations
def continuous_map.to_ae_eq_fun {α : Type u_1} {β : Type u_2} [measurable_space α] (μ : measure_theory.measure α) [topological_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] (f : C(α, β)) :
α →ₘ[μ] β

The equivalence class of μ-almost-everywhere measurable functions associated to a continuous map.

Equations

The add_hom from the group of continuous maps from α to β to the group of equivalence classes of μ-almost-everywhere measurable functions.

Equations

The mul_hom from the group of continuous maps from α to β to the group of equivalence classes of μ-almost-everywhere measurable functions.

Equations

The linear map from the group of continuous maps from α to β to the group of equivalence classes of μ-almost-everywhere measurable functions.

Equations