# mathlibdocumentation

measure_theory.ae_eq_fun

# 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 of L⁰ space, where α and β are measurable spaces and μ is a measure on α. f : α →ₘ β is a "function" in L⁰. In comments, [f] is also used to denote an L⁰ 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 on L⁰ 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] if f a ≤ g a for almost all a in domain. And α →ₘ β inherits the preorder and partial order of β.

TODO: Define sup and inf on L⁰ so that it forms a lattice. It seems that β must be a linear order, since otherwise f ⊔ g may not be a measurable function.

## Implementation notes #

• f.to_fun : To find a representative of f : α →ₘ β, use f.to_fun. For each operation op in L⁰, there is a lemma called op_to_fun, characterizing, say, (f op g).to_fun.
• ae_eq_fun.mk : To constructs an L⁰ function α →ₘ β from a measurable function f : α → β, use ae_eq_fun.mk
• comp : Use comp g f to get [g ∘ f] from g : β → γ and [f] : α →ₘ γ
• comp₂ : Use comp₂ 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) (μ : measure_theory.measure α) :
setoid {f // μ}

The equivalence relation of being almost everywhere equal

Equations
def measure_theory.ae_eq_fun (α : Type u_1) (β : Type u_2) (μ : 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
def measure_theory.ae_eq_fun.mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α → β) (hf : μ) :
α →ₘ[μ] β

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]
def measure_theory.ae_eq_fun.has_coe_to_fun {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :

A measurable representative of an ae_eq_fun [f]

Equations
@[protected]
theorem measure_theory.ae_eq_fun.measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
@[protected]
theorem measure_theory.ae_eq_fun.ae_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
@[simp]
theorem measure_theory.ae_eq_fun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α → β) (hf : μ) :
quot.mk setoid.r f, hf⟩ =
@[simp]
theorem measure_theory.ae_eq_fun.mk_eq_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f g : α → β} {hf : μ} {hg : μ} :
f =ᵐ[μ] g
@[simp]
theorem measure_theory.ae_eq_fun.mk_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
@[ext]
theorem measure_theory.ae_eq_fun.ext {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) :
f = g
theorem measure_theory.ae_eq_fun.ext_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f g : α →ₘ[μ] β} :
f = g f =ᵐ[μ] g
theorem measure_theory.ae_eq_fun.coe_fn_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α → β) (hf : μ) :
theorem measure_theory.ae_eq_fun.induction_on {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) {p : →ₘ[μ] β) → Prop} (H : ∀ (f : α → β) (hf : μ), p ) :
p f
theorem measure_theory.ae_eq_fun.induction_on₂ {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {α' : Type u_3} {β' : Type u_4} [measurable_space α'] [measurable_space β'] {μ' : measure_theory.measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : →ₘ[μ] β)(α' →ₘ[μ'] β') → Prop} (H : ∀ (f : α → β) (hf : μ) (f' : α' → β') (hf' : μ'), p hf')) :
p f f'
theorem measure_theory.ae_eq_fun.induction_on₃ {α : Type u_1} {β : Type u_2} {μ : 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} (H : ∀ (f : α → β) (hf : μ) (f' : α' → β') (hf' : μ') (f'' : α'' → β'') (hf'' : μ''), p hf') hf'')) :
p f f' f''
def measure_theory.ae_eq_fun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (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
• = (λ (f : {f // μ}), _) _
@[simp]
theorem measure_theory.ae_eq_fun.comp_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α → β) (hf : μ) :
= _
theorem measure_theory.ae_eq_fun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
= _
theorem measure_theory.ae_eq_fun.coe_fn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
f) =ᵐ[μ] g f
def measure_theory.ae_eq_fun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
α →ₘ[μ] β × γ

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

Equations
@[simp]
theorem measure_theory.ae_eq_fun.pair_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (f : α → β) (hf : μ) (g : α → γ) (hg : μ) :
.pair = 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} {μ : 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} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
(f.pair g) =ᵐ[μ] λ (x : α), (f x, g x)
def measure_theory.ae_eq_fun.comp₂ {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} (g : β → γ → δ) (hg : measurable ) (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
• f₂ = (f₁.pair f₂)
@[simp]
theorem measure_theory.ae_eq_fun.comp₂_mk_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} (g : β → γ → δ) (hg : measurable ) (f₁ : α → β) (f₂ : α → γ) (hf₁ : μ) (hf₂ : μ) :
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} {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} (g : β → γ → δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₂ = (f₁.pair f₂)
theorem measure_theory.ae_eq_fun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} (g : β → γ → δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (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} {μ : measure_theory.measure α} {γ : Type u_3} {δ : Type u_4} (g : β → γ → δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₁ f₂) =ᵐ[μ] λ (a : α), g (f₁ a) (f₂ a)
def measure_theory.ae_eq_fun.to_germ {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
μ.ae.germ β

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

Equations
• f.to_germ = (λ (f : {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} {μ : measure_theory.measure α} (f : α → β) (hf : μ) :
= f
theorem measure_theory.ae_eq_fun.to_germ_eq {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
theorem measure_theory.ae_eq_fun.to_germ_injective {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :
theorem measure_theory.ae_eq_fun.comp_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
f).to_germ =
theorem measure_theory.ae_eq_fun.comp₂_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β → γ → δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₁ f₂).to_germ = f₂.to_germ
def measure_theory.ae_eq_fun.lift_pred {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (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} {μ : measure_theory.measure α} (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} {μ : measure_theory.measure α} {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf : μ} {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} {μ : measure_theory.measure α} {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
∀ᵐ (a : α) ∂μ, r (f a) (g a)
@[protected, instance]
def measure_theory.ae_eq_fun.preorder {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [preorder β] :
preorder →ₘ[μ] β)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_le_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [preorder β] {f g : α → β} (hf : μ) (hg : μ) :
f ≤ᵐ[μ] g
@[simp, norm_cast]
theorem measure_theory.ae_eq_fun.coe_fn_le {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [preorder β] {f g : α →ₘ[μ] β} :
@[protected, instance]
def measure_theory.ae_eq_fun.partial_order {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :
Equations
def measure_theory.ae_eq_fun.const (α : Type u_1) {β : Type u_2} {μ : measure_theory.measure α} (b : β) :
α →ₘ[μ] β

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

Equations
theorem measure_theory.ae_eq_fun.coe_fn_const (α : Type u_1) {β : Type u_2} {μ : measure_theory.measure α} (b : β) :
@[protected, instance]
def measure_theory.ae_eq_fun.inhabited {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [inhabited β] :
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_zero β] :
has_zero →ₘ[μ] β)
@[protected, instance]
def measure_theory.ae_eq_fun.has_one {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_one β] :
has_one →ₘ[μ] β)
Equations
theorem measure_theory.ae_eq_fun.one_def {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_one β] :
theorem measure_theory.ae_eq_fun.zero_def {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_zero β] :
theorem measure_theory.ae_eq_fun.coe_fn_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_zero β] :
0 =ᵐ[μ] 0
theorem measure_theory.ae_eq_fun.coe_fn_one {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_one β] :
1 =ᵐ[μ] 1
@[simp]
theorem measure_theory.ae_eq_fun.zero_to_germ {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_zero β] :
@[simp]
theorem measure_theory.ae_eq_fun.one_to_germ {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_one β] :
@[protected, instance]
def measure_theory.ae_eq_fun.has_add {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_monoid γ]  :
@[protected, instance]
def measure_theory.ae_eq_fun.has_mul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [monoid γ]  :
has_mul →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_mul_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [monoid γ] (f g : α → γ) (hf : μ) (hg : μ) :
= _
@[simp]
theorem measure_theory.ae_eq_fun.mk_add_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_monoid γ] (f g : α → γ) (hf : μ) (hg : μ) :
= _
theorem measure_theory.ae_eq_fun.coe_fn_mul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [monoid γ] (f g : α →ₘ[μ] γ) :
f * g =ᵐ[μ] (f) * g
theorem measure_theory.ae_eq_fun.coe_fn_add {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_monoid γ] (f g : α →ₘ[μ] γ) :
(f + g) =ᵐ[μ] f + g
@[simp]
theorem measure_theory.ae_eq_fun.mul_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [monoid γ] (f g : α →ₘ[μ] γ) :
(f * g).to_germ = (f.to_germ) * g.to_germ
@[simp]
theorem measure_theory.ae_eq_fun.add_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_monoid γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.add_monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_monoid γ]  :
@[protected, instance]
def measure_theory.ae_eq_fun.monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [monoid γ]  :
monoid →ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.add_comm_monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ]  :
@[protected, instance]
def measure_theory.ae_eq_fun.comm_monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [comm_monoid γ]  :
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_neg {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ]  :
has_neg →ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.has_inv {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ]  :
has_inv →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.neg_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f : α → γ) (hf : μ) :
@[simp]
theorem measure_theory.ae_eq_fun.inv_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f : α → γ) (hf : μ) :
theorem measure_theory.ae_eq_fun.coe_fn_inv {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.coe_fn_neg {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.neg_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.inv_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.has_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ]  :
has_sub →ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.has_div {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ]  :
has_div →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_div {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f g : α → γ) (hf : ae_measurable (λ (a : α), f a) μ) (hg : ae_measurable (λ (a : α), g a) μ) :
_ =
theorem measure_theory.ae_eq_fun.mk_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f g : α → γ) (hf : ae_measurable (λ (a : α), f a) μ) (hg : ae_measurable (λ (a : α), g a) μ) :
_ =
theorem measure_theory.ae_eq_fun.coe_fn_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f g : α →ₘ[μ] γ) :
(f - g) =ᵐ[μ] f - g
theorem measure_theory.ae_eq_fun.coe_fn_div {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f g : α →ₘ[μ] γ) :
(f / g) =ᵐ[μ] f / g
theorem measure_theory.ae_eq_fun.sub_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ] (f g : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.div_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [group γ]  :
group →ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.add_group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [add_group γ]  :
@[protected, instance]
def measure_theory.ae_eq_fun.add_comm_group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ]  :
@[protected, instance]
def measure_theory.ae_eq_fun.comm_group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space γ] [comm_group γ]  :
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_scalar {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ] :
→ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.smul_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ] (c : 𝕜) (f : α → γ) (hf : μ) :
= _
theorem measure_theory.ae_eq_fun.coe_fn_smul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f) =ᵐ[μ] c f
theorem measure_theory.ae_eq_fun.smul_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).to_germ = c f.to_germ
@[protected, instance]
def measure_theory.ae_eq_fun.module {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ]  :
→ₘ[μ] γ)
Equations

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

Equations
@[simp]
theorem measure_theory.ae_eq_fun.lintegral_mk {α : Type u_1} {μ : measure_theory.measure α} (f : α → ℝ≥0∞) (hf : μ) :
= ∫⁻ (a : α), f a μ
theorem measure_theory.ae_eq_fun.lintegral_coe_fn {α : Type u_1} {μ : measure_theory.measure α} (f : α →ₘ[μ] ℝ≥0∞) :
∫⁻ (a : α), f a μ = f.lintegral
@[simp]
@[simp]
theorem measure_theory.ae_eq_fun.lintegral_add {α : Type u_1} {μ : measure_theory.measure α} (f g : α →ₘ[μ] ℝ≥0∞) :
(f + g).lintegral =
theorem measure_theory.ae_eq_fun.lintegral_mono {α : Type u_1} {μ : measure_theory.measure α} {f g : α →ₘ[μ] ℝ≥0∞} :
f g
def measure_theory.ae_eq_fun.pos_part {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [linear_order γ] [has_zero γ] (f : α →ₘ[μ] γ) :
α →ₘ[μ] γ

Positive part of an ae_eq_fun.

Equations
@[simp]
theorem measure_theory.ae_eq_fun.pos_part_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [linear_order γ] [has_zero γ] (f : α → γ) (hf : μ) :
= 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} {μ : measure_theory.measure α} [linear_order γ] [has_zero γ] (f : α →ₘ[μ] γ) :
(f.pos_part) =ᵐ[μ] λ (a : α), max (f a) 0
def continuous_map.to_ae_eq_fun {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) [borel_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} (μ : measure_theory.measure α) [borel_space α] [borel_space β] (f : C(α, β)) :
def continuous_map.to_ae_eq_fun_add_hom {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) [borel_space α] [borel_space β] [add_group β]  :
C(α, β) →+ α →ₘ[μ] β

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} (μ : measure_theory.measure α) [borel_space α] [borel_space β] [group β]  :
C(α, β) →* α →ₘ[μ] β

The mul_hom from the group of continuous maps from α to β to the group of equivalence classes of μ-almost-everywhere measurable functions.

Equations
def continuous_map.to_ae_eq_fun_linear_map {α : Type u_1} {γ : Type u_3} (μ : measure_theory.measure α) [borel_space α] {𝕜 : Type u_5} [semiring 𝕜] [borel_space γ] [ γ] [ γ]  :
C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ

The linear map from the group of continuous maps from α to β to the group of equivalence classes of μ`-almost-everywhere measurable functions.

Equations