# mathlibdocumentation

measure_theory.ae_eq_fun_metric

# Emetric space structure on almost everywhere equal functions #

Emetric on L⁰ : If β is an emetric_space, then L⁰ can be made into an emetric_space, where edist [f] [g] is defined to be ∫⁻ a, edist (f a) (g a).

The integral used here is lintegral : (α → ℝ≥0∞) → ℝ≥0∞, which is defined in the file
integration.lean.

See edist_mk_mk and edist_to_fun.


TODO: remove this file, and use instead the more general Lp space specialized to p = 1.

def measure_theory.ae_eq_fun.edist {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} (f g : α →ₘ[μ] γ) :

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

Equations
theorem measure_theory.ae_eq_fun.edist_comm {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} (f g : α →ₘ[μ] γ) :
f.edist g = g.edist f
theorem measure_theory.ae_eq_fun.coe_fn_edist {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} (f g : α →ₘ[μ] γ) :
(f.edist g) =ᵐ[μ] λ (a : α), edist (f a) (g a)
theorem measure_theory.ae_eq_fun.edist_self {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} (f : α →ₘ[μ] γ) :
f.edist f = 0
@[instance]
def measure_theory.ae_eq_fun.emetric_space {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α}  :

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_mk_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {f g : α → γ} (hf : μ) (hg : μ) :
= ∫⁻ (x : α), edist (f x) (g x) μ
theorem measure_theory.ae_eq_fun.edist_eq_coe {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} (f g : α →ₘ[μ] γ) :
g = ∫⁻ (x : α), edist (f x) (g x) μ
theorem measure_theory.ae_eq_fun.edist_zero_eq_coe {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_zero γ] (f : α →ₘ[μ] γ) :
0 = ∫⁻ (x : α), edist (f x) 0 μ
theorem measure_theory.ae_eq_fun.edist_mk_mk' {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [metric_space γ] {f g : α → γ} (hf : μ) (hg : μ) :
= ∫⁻ (x : α), (nndist (f x) (g x)) μ
theorem measure_theory.ae_eq_fun.edist_eq_coe' {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [metric_space γ] (f g : α →ₘ[μ] γ) :
g = ∫⁻ (x : α), (nndist (f x) (g x)) μ
theorem measure_theory.ae_eq_fun.edist_add_right {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group γ] [borel_space γ] (f g h : α →ₘ[μ] γ) :
edist (f + h) (g + h) = g
theorem measure_theory.ae_eq_fun.edist_smul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [normed_group γ] [ γ] [borel_space γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
edist (c f) 0 = * 0