mathlib documentation

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.

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 α] {μ : measure_theory.measure α} [measurable_space γ] [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 α] {μ : measure_theory.measure α} [measurable_space γ] [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 α] {μ : measure_theory.measure α} [measurable_space γ] {𝕜 : Type u_5} [normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] [normed_group γ] [topological_space.second_countable_topology γ] [normed_space 𝕜 γ] [borel_space γ] (c : 𝕜) (f : α →ₘ[μ] γ) :