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_fun -
The 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.
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 // ae_measurable f μ}
The equivalence relation of being almost everywhere equal
Equations
- measure_theory.measure.ae_eq_setoid β μ = {r := λ (f g : {f // ae_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 α]
{μ : 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
- measure_theory.ae_eq_fun.mk f hf = quotient.mk' ⟨f, hf⟩
@[protected, 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 (α →ₘ[μ] β)
A measurable representative of an ae_eq_fun [f]
Equations
- measure_theory.ae_eq_fun.has_coe_to_fun = {F := λ (f : α →ₘ[μ] β), α → β, coe := λ (f : α →ₘ[μ] β), ae_measurable.mk (quotient.out' f).val _}
@[protected]
theorem
measure_theory.ae_eq_fun.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
(f : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.ae_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
(f : α →ₘ[μ] β) :
ae_measurable ⇑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 μ) :
quot.mk setoid.r ⟨f, hf⟩ = measure_theory.ae_eq_fun.mk f hf
@[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 μ} :
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 α]
{μ : 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 : α →ₘ[μ] β} :
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 μ) :
⇑(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 α]
{μ : 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
- measure_theory.ae_eq_fun.comp g hg f = quotient.lift_on' f (λ (f : {f // ae_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 α]
{μ : measure_theory.measure α}
[measurable_space β]
[measurable_space γ]
(g : β → γ)
(hg : measurable g)
(f : α → β)
(hf : ae_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 α]
{μ : measure_theory.measure α}
[measurable_space β]
[measurable_space γ]
(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 α]
{μ : 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
- f.pair g = quotient.lift_on₂' f g (λ (f : {f // ae_measurable f μ}) (g : {f // ae_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 α]
{μ : measure_theory.measure α}
[measurable_space β]
[measurable_space γ]
(f : α → β)
(hf : ae_measurable f μ)
(g : α → γ)
(hg : ae_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 α]
{μ : 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 : α →ₘ[μ] γ) :
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
- 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 α]
{μ : 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₂ μ) :
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 α]
{μ : 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.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 α]
{μ : 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₂ : α →ₘ[μ] γ) :
def
measure_theory.ae_eq_fun.to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
(f : α →ₘ[μ] β) :
Interpret f : α →ₘ[μ] β as a germ at μ.ae forgetting that f is almost everywhere
measurable.
Equations
- f.to_germ = quotient.lift_on' f (λ (f : {f // ae_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 α]
{μ : measure_theory.measure α}
[measurable_space β]
(f : α → β)
(hf : ae_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 α]
{μ : measure_theory.measure α}
[measurable_space β]
(f : α →ₘ[μ] β) :
theorem
measure_theory.ae_eq_fun.to_germ_injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β] :
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 : α →ₘ[μ] β) :
(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 α]
{μ : measure_theory.measure α}
[measurable_space β]
[measurable_space γ]
[measurable_space δ]
(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 α]
{μ : 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 μ} :
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 α]
{μ : 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)
@[protected, instance]
def
measure_theory.ae_eq_fun.preorder
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[preorder β] :
@[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 μ) :
measure_theory.ae_eq_fun.mk f hf ≤ measure_theory.ae_eq_fun.mk g hg ↔ 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 α}
[measurable_space β]
[preorder β]
{f g : α →ₘ[μ] β} :
@[protected, instance]
def
measure_theory.ae_eq_fun.partial_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[partial_order β] :
partial_order (α →ₘ[μ] β)
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
- measure_theory.ae_eq_fun.const α b = measure_theory.ae_eq_fun.mk (λ (a : α), b) ae_measurable_const
theorem
measure_theory.ae_eq_fun.coe_fn_const
(α : Type u_1)
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
(b : β) :
⇑(measure_theory.ae_eq_fun.const α b) =ᵐ[μ] function.const α b
@[protected, instance]
def
measure_theory.ae_eq_fun.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[inhabited β] :
Equations
@[protected, instance]
def
measure_theory.ae_eq_fun.has_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_zero β] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_one β] :
Equations
theorem
measure_theory.ae_eq_fun.one_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_one β] :
1 = measure_theory.ae_eq_fun.mk (λ (a : α), 1) ae_measurable_const
theorem
measure_theory.ae_eq_fun.zero_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_zero β] :
0 = measure_theory.ae_eq_fun.mk (λ (a : α), 0) ae_measurable_const
theorem
measure_theory.ae_eq_fun.coe_fn_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_zero β] :
theorem
measure_theory.ae_eq_fun.coe_fn_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
[has_one β] :
@[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 β] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_add
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_mul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[has_continuous_mul γ]
(f g : α → γ)
(hf : ae_measurable f μ)
(hg : ae_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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f g : α → γ)
(hf : ae_measurable f μ)
(hg : ae_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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[monoid γ]
[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 α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f g : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.add_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_monoid γ]
[has_continuous_add γ] :
add_monoid (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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
@[protected, instance]
def
measure_theory.ae_eq_fun.add_comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[topological_space.second_countable_topology γ]
[borel_space γ]
[add_comm_monoid γ]
[has_continuous_add γ] :
add_comm_monoid (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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
@[protected, instance]
def
measure_theory.ae_eq_fun.has_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_inv
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ] :
Equations
- measure_theory.ae_eq_fun.has_inv = {inv := measure_theory.ae_eq_fun.comp has_inv.inv measure_theory.ae_eq_fun.has_inv._proof_1}
@[simp]
theorem
measure_theory.ae_eq_fun.neg_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α → γ)
(hf : ae_measurable f μ) :
@[simp]
theorem
measure_theory.ae_eq_fun.inv_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ]
(f : α → γ)
(hf : ae_measurable f μ) :
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 : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.neg_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.inv_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_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 γ] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_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 γ] :
Equations
- measure_theory.ae_eq_fun.has_div = {div := measure_theory.ae_eq_fun.comp₂ has_div.div measure_theory.ae_eq_fun.has_div._proof_1}
@[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) μ) :
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.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) μ) :
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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_group γ]
[topological_add_group γ]
[topological_space.second_countable_topology γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_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 : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.sub_to_germ
{α : 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 : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.div_to_germ
{α : 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 : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.group
{α : 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 γ] :
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 measure_theory.ae_eq_fun.div_to_germ
@[protected, instance]
def
measure_theory.ae_eq_fun.add_group
{α : 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 γ] :
@[protected, instance]
def
measure_theory.ae_eq_fun.add_comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[borel_space γ]
[add_comm_group γ]
[topological_add_group γ]
[topological_space.second_countable_topology γ] :
add_comm_group (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[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 := _, npow := group.npow measure_theory.ae_eq_fun.group, npow_zero' := _, npow_succ' := _, inv := group.inv measure_theory.ae_eq_fun.group, div := group.div measure_theory.ae_eq_fun.group, div_eq_mul_inv := _, gpow := group.gpow measure_theory.ae_eq_fun.group, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, 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
- 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 α]
{μ : 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 μ) :
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 α]
{μ : 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 : α →ₘ[μ] γ) :
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 : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.module
{α : 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 𝕜 γ]
[topological_space.second_countable_topology γ]
[has_continuous_add γ] :
def
measure_theory.ae_eq_fun.lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →ₘ[μ] ℝ≥0∞) :
For f : α → ℝ≥0∞, define ∫ [f] to be ∫ f
Equations
- f.lintegral = quotient.lift_on' f (λ (f : {f // ae_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 : α → ℝ≥0∞)
(hf : ae_measurable f μ) :
theorem
measure_theory.ae_eq_fun.lintegral_coe_fn
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →ₘ[μ] ℝ≥0∞) :
@[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 : α →ₘ[μ] ℝ≥0∞} :
theorem
measure_theory.ae_eq_fun.lintegral_add
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f g : α →ₘ[μ] ℝ≥0∞) :
theorem
measure_theory.ae_eq_fun.lintegral_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α →ₘ[μ] ℝ≥0∞} :
def
measure_theory.ae_eq_fun.pos_part
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ]
(f : α →ₘ[μ] γ) :
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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ]
(f : α → γ)
(hf : ae_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 α]
{μ : measure_theory.measure α}
[measurable_space γ]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[topological_space.second_countable_topology γ]
[has_zero γ]
[opens_measurable_space γ]
(f : α →ₘ[μ] γ) :
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
theorem
continuous_map.coe_fn_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(α, β)) :
⇑(continuous_map.to_ae_eq_fun μ f) =ᵐ[μ] ⇑f
def
continuous_map.to_ae_eq_fun_add_hom
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
[add_group β]
[topological_add_group β]
[topological_space.second_countable_topology β] :
The add_hom from the group of continuous maps from α to β to the group of
equivalence classes of μ-almost-everywhere measurable functions.
def
continuous_map.to_ae_eq_fun_mul_hom
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[measurable_space β]
[borel_space β]
[group β]
[topological_group β]
[topological_space.second_countable_topology β] :
The mul_hom from the group of continuous maps from α to β to the group of equivalence
classes of μ-almost-everywhere measurable functions.
Equations
- continuous_map.to_ae_eq_fun_mul_hom μ = {to_fun := continuous_map.to_ae_eq_fun μ _inst_6, map_one' := _, map_mul' := _}
def
continuous_map.to_ae_eq_fun_linear_map
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
{𝕜 : Type u_5}
[semiring 𝕜]
[topological_space 𝕜]
[measurable_space 𝕜]
[opens_measurable_space 𝕜]
[topological_space γ]
[measurable_space γ]
[borel_space γ]
[add_comm_group γ]
[module 𝕜 γ]
[topological_add_group γ]
[has_continuous_smul 𝕜 γ]
[topological_space.second_countable_topology γ] :
The linear map from the group of continuous maps from α to β to the group of equivalence
classes of μ-almost-everywhere measurable functions.
Equations
- continuous_map.to_ae_eq_fun_linear_map μ = {to_fun := (continuous_map.to_ae_eq_fun_add_hom μ).to_fun, map_add' := _, map_smul' := _}