mathlib3 documentation

measure_theory.function.ae_eq_fun

Almost everywhere equal functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We build a space of equivalence classes of functions, where two 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. To use this space as a basis for the L^p spaces and for the Bochner integral, we consider equivalence classes of strongly measurable functions (or, equivalently, of almost everywhere strongly measurable functions.)

See l1_space.lean for space.

Notation #

Main statements #

Implementation notes #

Tags #

function space, almost everywhere equal, L⁰, ae_eq_fun

The equivalence relation of being almost everywhere equal for almost everywhere strongly measurable functions.

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

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

Equations
Instances for measure_theory.ae_eq_fun

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

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

A measurable representative of an ae_eq_fun [f]

Equations
@[ext]
theorem measure_theory.ae_eq_fun.ext {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_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 α} [topological_space β] {f g : α →ₘ[μ] β} :
f = g f =ᵐ[μ] g
theorem measure_theory.ae_eq_fun.induction_on {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] (f : α →ₘ[μ] β) {p : →ₘ[μ] β) Prop} (H : (f : α β) (hf : measure_theory.ae_strongly_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 α} [topological_space β] {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [topological_space β'] {μ' : measure_theory.measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : →ₘ[μ] β) (α' →ₘ[μ'] β') Prop} (H : (f : α β) (hf : measure_theory.ae_strongly_measurable f μ) (f' : α' β') (hf' : measure_theory.ae_strongly_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 α} [topological_space β] {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [topological_space β'] {μ' : measure_theory.measure α'} {α'' : Type u_5} {β'' : Type u_6} [measurable_space α''] [topological_space β''] {μ'' : measure_theory.measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'') {p : →ₘ[μ] β) (α' →ₘ[μ'] β') (α'' →ₘ[μ''] β'') Prop} (H : (f : α β) (hf : measure_theory.ae_strongly_measurable f μ) (f' : α' β') (hf' : measure_theory.ae_strongly_measurable f' μ') (f'' : α'' β'') (hf'' : measure_theory.ae_strongly_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 α} [topological_space β] [topological_space γ] (g : β γ) (hg : continuous g) (f : α →ₘ[μ] β) :
α →ₘ[μ] γ

Given a continuous 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
theorem measure_theory.ae_eq_fun.coe_fn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] (g : β γ) (hg : continuous 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] : α →ₘ γ. This requires that γ has a second countable topology.

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

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

Equations
theorem measure_theory.ae_eq_fun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_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 α} [topological_space β] [topological_space γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
(f.pair g) =ᵐ[μ] λ (x : α), (f x, g x)
def measure_theory.ae_eq_fun.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
α →ₘ[μ] δ

Given a continuous 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} {γ : Type u_3} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (function.uncurry g)) (f₁ : α β) (f₂ : α γ) (hf₁ : measure_theory.ae_strongly_measurable f₁ μ) (hf₂ : measure_theory.ae_strongly_measurable f₂ μ) :
theorem measure_theory.ae_eq_fun.comp₂_eq_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (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} {γ : Type u_3} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
(measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂) =ᵐ[μ] λ (a : α), g (f₁ a) (f₂ a)

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)] : α →ₘ γ. This requires δ to have second-countable topology.

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

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

Equations
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 α} [topological_space β] [topological_space γ] [topological_space δ] (g : β γ δ) (hg : continuous (function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
def measure_theory.ae_eq_fun.lift_pred {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_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 α} [topological_space β] [topological_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_iff_coe_fn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [topological_space γ] {r : β γ Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
@[simp, norm_cast]
theorem measure_theory.ae_eq_fun.coe_fn_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [preorder β] {f g : α →ₘ[μ] β} :
@[protected, instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_sup {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [semilattice_sup β] [has_continuous_sup β] (f g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] λ (x : α), f x g x
@[protected]
@[protected]
@[protected]
theorem measure_theory.ae_eq_fun.sup_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [semilattice_sup β] [has_continuous_sup β] (f g f' : α →ₘ[μ] β) (hf : f f') (hg : g f') :
f g f'
@[protected, instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_inf {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [semilattice_inf β] [has_continuous_inf β] (f g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] λ (x : α), f x g x
@[protected]
@[protected]
@[protected]
theorem measure_theory.ae_eq_fun.le_inf {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] [semilattice_inf β] [has_continuous_inf β] (f' f g : α →ₘ[μ] β) (hf : f' f) (hg : f' g) :
f' f g
def measure_theory.ae_eq_fun.const (α : Type u_1) {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [topological_space β] (b : β) :
α →ₘ[μ] β

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

Equations
@[simp]
@[protected, instance]
def measure_theory.ae_eq_fun.has_smul {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] {𝕜 : Type u_5} [has_smul 𝕜 γ] [has_continuous_const_smul 𝕜 γ] :
has_smul 𝕜 →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.coe_fn_smul {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] {𝕜 : Type u_5} [has_smul 𝕜 γ] [has_continuous_const_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 α} [topological_space γ] {𝕜 : Type u_5} [has_smul 𝕜 γ] [has_continuous_const_smul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).to_germ = c f.to_germ
@[protected, instance]
def measure_theory.ae_eq_fun.smul_comm_class {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] {𝕜 : Type u_5} {𝕜' : Type u_6} [has_smul 𝕜 γ] [has_continuous_const_smul 𝕜 γ] [has_smul 𝕜' γ] [has_continuous_const_smul 𝕜' γ] [smul_comm_class 𝕜 𝕜' γ] :
smul_comm_class 𝕜 𝕜' →ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.is_scalar_tower {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] {𝕜 : Type u_5} {𝕜' : Type u_6} [has_smul 𝕜 γ] [has_continuous_const_smul 𝕜 γ] [has_smul 𝕜' γ] [has_continuous_const_smul 𝕜' γ] [has_smul 𝕜 𝕜'] [is_scalar_tower 𝕜 𝕜' γ] :
is_scalar_tower 𝕜 𝕜' →ₘ[μ] γ)
@[protected, instance]
theorem measure_theory.ae_eq_fun.coe_fn_mul {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [has_mul γ] [has_continuous_mul γ] (f g : α →ₘ[μ] γ) :
(f * g) =ᵐ[μ] f * g
theorem measure_theory.ae_eq_fun.coe_fn_add {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [has_add γ] [has_continuous_add γ] (f g : α →ₘ[μ] γ) :
(f + g) =ᵐ[μ] f + g
@[simp]
theorem measure_theory.ae_eq_fun.mul_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [has_mul γ] [has_continuous_mul γ] (f g : α →ₘ[μ] γ) :
@[simp]
theorem measure_theory.ae_eq_fun.add_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [has_add γ] [has_continuous_add γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_pow {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [monoid γ] [has_continuous_mul γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem measure_theory.ae_eq_fun.pow_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [monoid γ] [has_continuous_mul γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).to_germ = f.to_germ ^ n
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_div {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [group γ] [topological_group γ] (f g : α →ₘ[μ] γ) :
(f / g) =ᵐ[μ] f / g
theorem measure_theory.ae_eq_fun.div_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [group γ] [topological_group γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
Equations
theorem measure_theory.ae_eq_fun.coe_fn_zpow {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [group γ] [topological_group γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem measure_theory.ae_eq_fun.zpow_to_germ {α : Type u_1} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [topological_space γ] [group γ] [topological_group γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).to_germ = f.to_germ ^ n
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
noncomputable def measure_theory.ae_eq_fun.lintegral {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α →ₘ[μ] ennreal) :

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

Equations

Positive part of an ae_eq_fun.

Equations

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