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 L¹ space.
Notation
α →ₘ[μ] βis the type ofL⁰space, whereαandβare measurable spaces andμis a measure onα.f : α →ₘ βis a "function" inL⁰. In comments,[f]is also used to denote anL⁰function.ₘcan be typed as\_m. Sometimes it is shown as a box if font is missing.
Main statements
The linear structure of
L⁰: Addition and scalar multiplication are defined onL⁰in the natural way, i.e.,[f] + [g] := [f + g],c • [f] := [c • f]. So defined,α →ₘ βinherits the linear structure ofβ. For example, ifβis a module, thenα →ₘ βis a module over the same ring.See
mk_add_mk,neg_mk,mk_sub_mk,smul_mk,add_to_fun,neg_to_fun,sub_to_fun,smul_to_funThe order structure of
L⁰:≤can be defined in a similar way:[f] ≤ [g]iff a ≤ g afor almost allain domain. Andα →ₘ βinherits the preorder and partial order ofβ.TODO: Define
supandinfonL⁰so that it forms a lattice. It seems thatβmust be a linear order, since otherwisef ⊔ gmay not be a measurable function.Emetric on
L⁰: Ifβis anemetric_space, thenL⁰can be made into anemetric_space, whereedist [f] [g]is defined to be∫⁻ a, edist (f a) (g a).The integral used here is
lintegral : (α → ennreal) → ennreal, which is defined in the fileintegration.lean.See
edist_mk_mkandedist_to_fun.
Implementation notes
f.to_fun: To find a representative off : α →ₘ β, usef.to_fun. For each operationopinL⁰, there is a lemma calledop_to_fun, characterizing, say,(f op g).to_fun.ae_eq_fun.mk: To constructs anL⁰functionα →ₘ βfrom a measurable functionf : α → β, useae_eq_fun.mkcomp: Usecomp g fto get[g ∘ f]fromg : β → γand[f] : α →ₘ γcomp₂: Usecomp₂ g f₁ f₂ to get[λa, g (f₁ a) (f₂ a)]. For example,[f + g]iscomp₂ (+)`
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 // measurable f}
The equivalence relation of being almost everywhere equal
Equations
- measure_theory.measure.ae_eq_setoid β μ = {r := λ (f g : {f // measurable f}), ↑f =ᵐ[μ] ↑g, iseqv := _}
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
- (α →ₘ[μ] β) = quotient (measure_theory.measure.ae_eq_setoid β μ)
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
- measure_theory.ae_eq_fun.mk f hf = quotient.mk' ⟨f, hf⟩
@[instance]
def
measure_theory.ae_eq_fun.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α} :
has_coe_to_fun (α →ₘ[μ] β)
A representative of an ae_eq_fun [f]
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) :
quot.mk setoid.r ⟨f, hf⟩ = measure_theory.ae_eq_fun.mk f hf
@[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 : α →ₘ[μ] β) :
quotient.out' f = ⟨⇑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} :
measure_theory.ae_eq_fun.mk f hf = measure_theory.ae_eq_fun.mk g hg ↔ f =ᵐ[μ] 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 : α →ₘ[μ] β} :
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) :
⇑(measure_theory.ae_eq_fun.mk f hf) =ᵐ[μ] 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
- measure_theory.ae_eq_fun.comp g hg f = quotient.lift_on' f (λ (f : {f // measurable f}), measure_theory.ae_eq_fun.mk (g ∘ ↑f) _) _
@[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) :
measure_theory.ae_eq_fun.comp g hg (measure_theory.ae_eq_fun.mk f hf) = measure_theory.ae_eq_fun.mk (g ∘ 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 : α →ₘ[μ] β) :
measure_theory.ae_eq_fun.comp g hg f = measure_theory.ae_eq_fun.mk (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
- f.pair g = quotient.lift_on₂' f g (λ (f : {f // measurable f}) (g : {f // measurable f}), measure_theory.ae_eq_fun.mk (λ (x : α), (f.val x, g.val x)) _) measure_theory.ae_eq_fun.pair._proof_2
@[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) :
(measure_theory.ae_eq_fun.mk f hf).pair (measure_theory.ae_eq_fun.mk g hg) = measure_theory.ae_eq_fun.mk (λ (x : α), (f x, g x)) _
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 : α →ₘ[μ] γ) :
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
- measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.comp (function.uncurry g) hg (f₁.pair f₂)
@[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₂) :
measure_theory.ae_eq_fun.comp₂ g hg (measure_theory.ae_eq_fun.mk f₁ hf₁) (measure_theory.ae_eq_fun.mk f₂ hf₂) = measure_theory.ae_eq_fun.mk (λ (a : α), g (f₁ a) (f₂ a)) _
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₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.comp (function.uncurry g) hg (f₁.pair 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₂ : α →ₘ[μ] γ) :
def
measure_theory.ae_eq_fun.to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α} :
Interpret f : α →ₘ[μ] β as a germ at μ.ae forgetting that f is measurable.
Equations
- f.to_germ = quotient.lift_on' f (λ (f : {f // measurable f}), ↑↑f) measure_theory.ae_eq_fun.to_germ._proof_1
@[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) :
(measure_theory.ae_eq_fun.mk f hf).to_germ = ↑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.to_germ_injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α} :
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 : α →ₘ[μ] β) :
(measure_theory.ae_eq_fun.comp g hg f).to_germ = filter.germ.map g f.to_germ
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₂ : α →ₘ[μ] γ) :
(measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂).to_germ = filter.germ.map₂ g f₁.to_germ f₂.to_germ
def
measure_theory.ae_eq_fun.lift_pred
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α} :
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 α} :
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} :
measure_theory.ae_eq_fun.lift_rel r (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (f a) (g a)
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)
@[instance]
def
measure_theory.ae_eq_fun.preorder
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[preorder β] :
@[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) :
measure_theory.ae_eq_fun.mk f hf ≤ measure_theory.ae_eq_fun.mk g hg ↔ f ≤ᵐ[μ] 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 : α →ₘ[μ] β} :
@[instance]
def
measure_theory.ae_eq_fun.partial_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[partial_order β] :
partial_order (α →ₘ[μ] β)
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
- measure_theory.ae_eq_fun.const α b = measure_theory.ae_eq_fun.mk (λ (a : α), b) measurable_const
theorem
measure_theory.ae_eq_fun.coe_fn_const
(α : Type u_1)
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
(b : β) :
⇑(measure_theory.ae_eq_fun.const α b) =ᵐ[μ] function.const α b
@[instance]
def
measure_theory.ae_eq_fun.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[inhabited β] :
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 β] :
@[instance]
def
measure_theory.ae_eq_fun.has_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[has_one β] :
Equations
theorem
measure_theory.ae_eq_fun.zero_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[has_zero β] :
0 = measure_theory.ae_eq_fun.mk (λ (a : α), 0) measurable_const
theorem
measure_theory.ae_eq_fun.one_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[has_one β] :
1 = measure_theory.ae_eq_fun.mk (λ (a : α), 1) measurable_const
theorem
measure_theory.ae_eq_fun.coe_fn_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[has_one β] :
theorem
measure_theory.ae_eq_fun.coe_fn_zero
{α : 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 β] :
@[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 β] :
@[instance]
def
measure_theory.ae_eq_fun.has_add
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ] :
@[instance]
def
measure_theory.ae_eq_fun.has_mul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ] :
Equations
- measure_theory.ae_eq_fun.has_mul = {mul := measure_theory.ae_eq_fun.comp₂ has_mul.mul measure_theory.ae_eq_fun.has_mul._proof_1}
@[simp]
theorem
measure_theory.ae_eq_fun.mk_mul_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ]
(f g : α → γ)
(hf : measurable f)
(hg : measurable g) :
measure_theory.ae_eq_fun.mk f hf * measure_theory.ae_eq_fun.mk g hg = measure_theory.ae_eq_fun.mk (f * g) _
@[simp]
theorem
measure_theory.ae_eq_fun.mk_add_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f g : α → γ)
(hf : measurable f)
(hg : measurable g) :
measure_theory.ae_eq_fun.mk f hf + measure_theory.ae_eq_fun.mk g hg = measure_theory.ae_eq_fun.mk (f + g) _
theorem
measure_theory.ae_eq_fun.coe_fn_mul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_add
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f g : α →ₘ[μ] γ) :
@[simp]
theorem
measure_theory.ae_eq_fun.add_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f g : α →ₘ[μ] γ) :
@[simp]
theorem
measure_theory.ae_eq_fun.mul_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ]
(f g : α →ₘ[μ] γ) :
@[instance]
def
measure_theory.ae_eq_fun.monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ] :
Equations
- measure_theory.ae_eq_fun.monoid = function.injective.monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.monoid._proof_1 measure_theory.ae_eq_fun.mul_to_germ
@[instance]
def
measure_theory.ae_eq_fun.add_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ] :
add_monoid (α →ₘ[μ] γ)
@[instance]
def
measure_theory.ae_eq_fun.add_comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_comm_monoid γ]
[has_continuous_add γ] :
add_comm_monoid (α →ₘ[μ] γ)
@[instance]
def
measure_theory.ae_eq_fun.comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[comm_monoid γ]
[has_continuous_mul γ] :
comm_monoid (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.comm_monoid = function.injective.comm_monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.comm_monoid._proof_1 measure_theory.ae_eq_fun.comm_monoid._proof_2
@[instance]
def
measure_theory.ae_eq_fun.has_inv
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ] :
@[instance]
def
measure_theory.ae_eq_fun.has_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ] :
@[simp]
theorem
measure_theory.ae_eq_fun.neg_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α → γ)
(hf : measurable f) :
@[simp]
theorem
measure_theory.ae_eq_fun.inv_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ]
(f : α → γ)
(hf : measurable f) :
theorem
measure_theory.ae_eq_fun.coe_fn_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
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 : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.inv_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.neg_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
@[instance]
def
measure_theory.ae_eq_fun.group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ]
[topological_space.second_countable_topology γ] :
Equations
- measure_theory.ae_eq_fun.group = function.injective.group measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.group._proof_1 measure_theory.ae_eq_fun.group._proof_2 measure_theory.ae_eq_fun.inv_to_germ
@[instance]
def
measure_theory.ae_eq_fun.add_group
{α : 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 γ] :
@[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)) :
measure_theory.ae_eq_fun.mk (f - g) _ = measure_theory.ae_eq_fun.mk f hf - measure_theory.ae_eq_fun.mk g hg
theorem
measure_theory.ae_eq_fun.coe_fn_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 : α →ₘ[μ] γ) :
@[instance]
def
measure_theory.ae_eq_fun.comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[comm_group γ]
[topological_group γ]
[topological_space.second_countable_topology γ] :
comm_group (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.comm_group = {mul := group.mul measure_theory.ae_eq_fun.group, mul_assoc := _, one := group.one measure_theory.ae_eq_fun.group, one_mul := _, mul_one := _, inv := group.inv measure_theory.ae_eq_fun.group, mul_left_inv := _, mul_comm := _}
@[instance]
def
measure_theory.ae_eq_fun.add_comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[borel_space γ]
[add_comm_group γ]
[topological_add_group γ]
[topological_space.second_countable_topology γ] :
add_comm_group (α →ₘ[μ] γ)
@[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
- measure_theory.ae_eq_fun.has_scalar = {smul := λ (c : 𝕜) (f : α →ₘ[μ] γ), measure_theory.ae_eq_fun.comp (has_scalar.smul c) _ f}
@[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) :
c • measure_theory.ae_eq_fun.mk f hf = measure_theory.ae_eq_fun.mk (c • 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 : α →ₘ[μ] γ) :
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 : α →ₘ[μ] γ) :
@[instance]
def
measure_theory.ae_eq_fun.semimodule
{α : 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 𝕜 γ]
[topological_space.second_countable_topology γ]
[has_continuous_add γ] :
semimodule 𝕜 (α →ₘ[μ] γ)
def
measure_theory.ae_eq_fun.lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
For f : α → ennreal, define ∫ [f] to be ∫ f
Equations
- f.lintegral = quotient.lift_on' f (λ (f : {f // measurable f}), ∫⁻ (a : α), ↑f a ∂μ) measure_theory.ae_eq_fun.lintegral._proof_1
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_mk
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → ennreal)
(hf : measurable f) :
theorem
measure_theory.ae_eq_fun.lintegral_coe_fn
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →ₘ[μ] ennreal) :
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_eq_zero_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α →ₘ[μ] ennreal} :
theorem
measure_theory.ae_eq_fun.lintegral_add
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f g : α →ₘ[μ] ennreal) :
theorem
measure_theory.ae_eq_fun.lintegral_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α →ₘ[μ] ennreal} :
def
measure_theory.ae_eq_fun.edist
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[emetric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ] :
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}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[emetric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ]
(f g : α →ₘ[μ] γ) :
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 : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.edist_self
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[emetric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ]
(f : α →ₘ[μ] γ) :
@[instance]
def
measure_theory.ae_eq_fun.emetric_space
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[emetric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ] :
emetric_space (α →ₘ[μ] γ)
Almost everywhere equal functions form an emetric_space, with the emetric defined as
edist f g = ∫⁻ a, edist (f a) (g a).
Equations
- measure_theory.ae_eq_fun.emetric_space = {to_has_edist := {edist := λ (f g : α →ₘ[μ] γ), (f.edist g).lintegral}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (f g : α →ₘ[μ] γ), (f.edist g).lintegral) measure_theory.ae_eq_fun.emetric_space._proof_5 measure_theory.ae_eq_fun.emetric_space._proof_6 measure_theory.ae_eq_fun.emetric_space._proof_7, uniformity_edist := _}
theorem
measure_theory.ae_eq_fun.edist_mk_mk
{α : 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 : α → γ}
(hf : measurable f)
(hg : measurable g) :
has_edist.edist (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk g hg) = ∫⁻ (x : α), has_edist.edist (f x) (g x) ∂μ
theorem
measure_theory.ae_eq_fun.edist_eq_coe
{α : 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 : α →ₘ[μ] γ) :
has_edist.edist f g = ∫⁻ (x : α), has_edist.edist (⇑f x) (⇑g x) ∂μ
theorem
measure_theory.ae_eq_fun.edist_zero_eq_coe
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[emetric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ]
[has_zero γ]
(f : α →ₘ[μ] γ) :
has_edist.edist f 0 = ∫⁻ (x : α), has_edist.edist (⇑f x) 0 ∂μ
theorem
measure_theory.ae_eq_fun.edist_mk_mk'
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[metric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ]
{f g : α → γ}
(hf : measurable f)
(hg : measurable g) :
has_edist.edist (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk g hg) = ∫⁻ (x : α), ↑(nndist (f x) (g x)) ∂μ
theorem
measure_theory.ae_eq_fun.edist_eq_coe'
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[metric_space γ]
[topological_space.second_countable_topology γ]
[opens_measurable_space γ]
(f g : α →ₘ[μ] γ) :
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 : α →ₘ[μ] γ) :
has_edist.edist (f + h) (g + h) = has_edist.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 : α →ₘ[μ] γ) :
has_edist.edist (c • f) 0 = ennreal.of_real ∥c∥ * has_edist.edist f 0
def
measure_theory.ae_eq_fun.pos_part
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[decidable_linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ] :
Positive part of an ae_eq_fun.
Equations
- f.pos_part = measure_theory.ae_eq_fun.comp (λ (x : γ), max x 0) measure_theory.ae_eq_fun.pos_part._proof_1 f
@[simp]
theorem
measure_theory.ae_eq_fun.pos_part_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[decidable_linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ]
(f : α → γ)
(hf : measurable f) :
(measure_theory.ae_eq_fun.mk f hf).pos_part = measure_theory.ae_eq_fun.mk (λ (x : α), max (f x) 0) _
theorem
measure_theory.ae_eq_fun.coe_fn_pos_part
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
[measurable_space γ]
{μ : measure_theory.measure α}
[topological_space γ]
[decidable_linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ]
(f : α →ₘ[μ] γ) :