# mathlib3documentation

measure_theory.function.ae_eq_fun

# Almost everywhere equal functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We build a space of equivalence classes of functions, where two 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. To use this space as a basis for the `L^p` spaces and for the Bochner integral, we consider equivalence classes of strongly measurable functions (or, equivalently, of almost everywhere strongly measurable functions.)

See `l1_space.lean` for `L¹` space.

## Notation #

• `α →ₘ[μ] β` is the type of `L⁰` space, where `α` is a measurable space, `β` is a topological space, 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 the coercion `(f : α → β)`, which is implemented as `f.to_fun`. For each operation `op` in `L⁰`, there is a lemma called `coe_fn_op`, characterizing, say, `(f op g : α → β)`.
• `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from an almost everywhere strongly measurable function `f : α → β`, use `ae_eq_fun.mk`
• `comp` : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ` when `g` is continuous. Use `comp_measurable` if `g` is only measurable (this requires the target space to be second countable).
• `comp₂` : Use `comp₂ g f₁ f₂ to get`[λ a, g (f₁ a) (f₂ a)]`. For example,`[f + g]`is`comp₂ (+)`

## 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 for almost everywhere strongly measurable functions.

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 almost everywhere strongly measurable functions, where two strongly measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure `0`.

Equations
Instances for `measure_theory.ae_eq_fun`
def measure_theory.ae_eq_fun.mk {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} (f : α β)  :
α →ₘ[μ] β

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]
noncomputable def measure_theory.ae_eq_fun.has_coe_to_fun {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :
has_coe_to_fun →ₘ[μ] β) (λ (_x : α →ₘ[μ] β), α β)

A measurable representative of an `ae_eq_fun` [f]

Equations
@[protected]
theorem measure_theory.ae_eq_fun.strongly_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
@[protected]
theorem measure_theory.ae_eq_fun.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α →ₘ[μ] β) :
@[protected]
theorem measure_theory.ae_eq_fun.measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [borel_space β] (f : α →ₘ[μ] β) :
@[protected]
theorem measure_theory.ae_eq_fun.ae_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [borel_space β] (f : α →ₘ[μ] β) :
@[simp]
theorem measure_theory.ae_eq_fun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α β)  :
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 : α β}  :
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 : α β)  :
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 α'] {μ' : 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 α'] {μ' : measure_theory.measure α'} {α'' : Type u_5} {β'' : Type u_6} [measurable_space α''] [topological_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 : continuous g) (f : α →ₘ[μ] β) :
α →ₘ[μ] γ

Given a continuous 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 : continuous g) (f : α β)  :
= _
theorem measure_theory.ae_eq_fun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β γ) (hg : continuous 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 : continuous g) (f : α →ₘ[μ] β) :
f) =ᵐ[μ] g f
def measure_theory.ae_eq_fun.comp_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [borel_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] : α →ₘ γ`. This requires that `γ` has a second countable topology.

Equations
• = (λ (f' : {f // , _) _
@[simp]
theorem measure_theory.ae_eq_fun.comp_measurable_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space β] (g : β γ) (hg : measurable g) (f : α β)  :
theorem measure_theory.ae_eq_fun.comp_measurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space β] (g : β γ) (hg : measurable g) (f : α →ₘ[μ] β) :
theorem measure_theory.ae_eq_fun.coe_fn_comp_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space β] (g : β γ) (hg : measurable g) (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 : α β) (g : α γ)  :
.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} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β γ δ) (hg : continuous ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
α →ₘ[μ] δ

Given a continuous 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} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β γ δ) (hg : continuous ) (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} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β γ δ) (hg : continuous ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₂ = (f₁.pair f₂)
theorem measure_theory.ae_eq_fun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β γ δ) (hg : continuous ) (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} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} (g : β γ δ) (hg : continuous ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₁ f₂) =ᵐ[μ] λ (a : α), g (f₁ a) (f₂ a)
def measure_theory.ae_eq_fun.comp₂_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (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)] : α →ₘ γ`. This requires `δ` to have second-countable topology.

Equations
@[simp]
theorem measure_theory.ae_eq_fun.comp₂_measurable_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (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₂_measurable_eq_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (g : β γ δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
= (f₁.pair f₂)
theorem measure_theory.ae_eq_fun.comp₂_measurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (g : β γ δ) (hg : measurable ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
= measure_theory.ae_eq_fun.mk (λ (a : α), g (f₁ a) (f₂ a)) _
theorem measure_theory.ae_eq_fun.coe_fn_comp₂_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (g : β γ δ) (hg : measurable ) (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 strongly 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 : α β)  :
= 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.comp_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} (g : β γ) (hg : continuous g) (f : α →ₘ[μ] β) :
f).to_germ =
theorem measure_theory.ae_eq_fun.comp_measurable_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [borel_space β] (g : β γ) (hg : measurable g) (f : α →ₘ[μ] β) :
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 : continuous ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
f₁ f₂).to_germ = f₂.to_germ
theorem measure_theory.ae_eq_fun.comp₂_measurable_to_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μ : measure_theory.measure α} [borel_space β] [borel_space γ] (g : β γ δ) (hg : measurable ) (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 : α γ}  :
∀ᵐ (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 : α β}  :
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]
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_sup {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :
has_sup →ₘ[μ] β)
Equations
theorem measure_theory.ae_eq_fun.coe_fn_sup {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] λ (x : α), f x g x
@[protected]
theorem measure_theory.ae_eq_fun.le_sup_left {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
f f g
@[protected]
theorem measure_theory.ae_eq_fun.le_sup_right {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
g f g
@[protected]
theorem measure_theory.ae_eq_fun.sup_le {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g f' : α →ₘ[μ] β) (hf : f f') (hg : g f') :
f g f'
@[protected, instance]
def measure_theory.ae_eq_fun.has_inf {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α}  :
has_inf →ₘ[μ] β)
Equations
theorem measure_theory.ae_eq_fun.coe_fn_inf {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] λ (x : α), f x g x
@[protected]
theorem measure_theory.ae_eq_fun.inf_le_left {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
f g f
@[protected]
theorem measure_theory.ae_eq_fun.inf_le_right {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f g : α →ₘ[μ] β) :
f g g
@[protected]
theorem measure_theory.ae_eq_fun.le_inf {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f' f g : α →ₘ[μ] β) (hf : f' f) (hg : f' g) :
f' f g
@[protected, instance]
def measure_theory.ae_eq_fun.lattice {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [lattice β]  :
lattice →ₘ[μ] β)
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 →ₘ[μ] β)
Equations
@[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_smul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ γ]  :
→ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.smul_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ γ] (c : 𝕜) (f : α γ)  :
= _
theorem measure_theory.ae_eq_fun.coe_fn_smul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ γ] (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} [ γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).to_germ = c f.to_germ
@[protected, instance]
def measure_theory.ae_eq_fun.smul_comm_class {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} {𝕜' : Type u_6} [ γ] [has_smul 𝕜' γ] [ 𝕜' γ] :
𝕜' →ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.is_scalar_tower {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} {𝕜' : Type u_6} [ γ] [has_smul 𝕜' γ] [ 𝕜'] [ 𝕜' γ] :
𝕜' →ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.is_central_scalar {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [ γ] [ γ] [ γ] :
→ₘ[μ] γ)
@[protected, instance]
def measure_theory.ae_eq_fun.has_add {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_add γ]  :
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_mul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_mul γ]  :
has_mul →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_mul_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_mul γ] (f g : α γ)  :
= _
@[simp]
theorem measure_theory.ae_eq_fun.mk_add_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_add γ] (f g : α γ)  :
= _
theorem measure_theory.ae_eq_fun.coe_fn_mul {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_mul γ] (f g : α →ₘ[μ] γ) :
(f * g) =ᵐ[μ] f * g
theorem measure_theory.ae_eq_fun.coe_fn_add {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_add γ] (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 α} [has_mul γ] (f g : α →ₘ[μ] γ) :
@[simp]
theorem measure_theory.ae_eq_fun.add_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [has_add γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.add_monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_monoid γ]  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.nat.has_pow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ]  :
has_pow →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_pow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ] (f : α γ) (n : ) :
= _
theorem measure_theory.ae_eq_fun.coe_fn_pow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem measure_theory.ae_eq_fun.pow_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).to_germ = f.to_germ ^ n
@[protected, instance]
def measure_theory.ae_eq_fun.monoid {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ]  :
monoid →ₘ[μ] γ)
Equations
def measure_theory.ae_eq_fun.to_germ_monoid_hom {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ]  :
→ₘ[μ] γ) →* μ.ae.germ γ

`ae_eq_fun.to_germ` as a `monoid_hom`.

Equations
def measure_theory.ae_eq_fun.to_germ_add_monoid_hom {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_monoid γ]  :
→ₘ[μ] γ) →+ μ.ae.germ γ

`ae_eq_fun.to_germ` as an `add_monoid_hom`.

Equations
@[simp]
theorem measure_theory.ae_eq_fun.to_germ_monoid_hom_apply {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [monoid γ] (f : α →ₘ[μ] γ) :
@[simp]
theorem measure_theory.ae_eq_fun.to_germ_add_monoid_hom_apply {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_monoid γ] (f : α →ₘ[μ] γ) :
@[protected, instance]
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_neg {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ]  :
has_neg →ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_inv {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ]  :
has_inv →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.neg_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ] (f : α γ)  :
@[simp]
theorem measure_theory.ae_eq_fun.inv_mk {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α γ)  :
theorem measure_theory.ae_eq_fun.coe_fn_inv {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.coe_fn_neg {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.neg_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ] (f : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.inv_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.has_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ]  :
has_sub →ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.has_div {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ]  :
has_div →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_div {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f g : α γ)  :
_ =
@[simp]
theorem measure_theory.ae_eq_fun.mk_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ] (f g : α γ)  :
_ =
theorem measure_theory.ae_eq_fun.coe_fn_sub {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [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 α} [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 α} [add_group γ] (f g : α →ₘ[μ] γ) :
theorem measure_theory.ae_eq_fun.div_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f g : α →ₘ[μ] γ) :
@[protected, instance]
def measure_theory.ae_eq_fun.has_int_pow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ]  :
has_pow →ₘ[μ] γ)
Equations
@[simp]
theorem measure_theory.ae_eq_fun.mk_zpow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α γ) (n : ) :
= _
theorem measure_theory.ae_eq_fun.coe_fn_zpow {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem measure_theory.ae_eq_fun.zpow_to_germ {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).to_germ = f.to_germ ^ n
@[protected, instance]
def measure_theory.ae_eq_fun.add_group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [add_group γ]  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [group γ]  :
group →ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.comm_group {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} [comm_group γ]  :
Equations
• measure_theory.ae_eq_fun.comm_group = measure_theory.ae_eq_fun.comm_group._proof_3 measure_theory.ae_eq_fun.comm_group._proof_4 measure_theory.ae_eq_fun.comm_group._proof_5 measure_theory.ae_eq_fun.comm_group._proof_6 measure_theory.ae_eq_fun.comm_group._proof_7 measure_theory.ae_eq_fun.comm_group._proof_8
@[protected, instance]
def measure_theory.ae_eq_fun.mul_action {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [monoid 𝕜] [ γ]  :
→ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.distrib_mul_action {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [monoid 𝕜] [add_monoid γ] [ γ]  :
→ₘ[μ] γ)
Equations
@[protected, instance]
def measure_theory.ae_eq_fun.module {α : Type u_1} {γ : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_5} [semiring 𝕜] [ γ]  :
→ₘ[μ] γ)
Equations
noncomputable def measure_theory.ae_eq_fun.lintegral {α : Type u_1} {μ : measure_theory.measure α} (f : α →ₘ[μ] ennreal) :

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 : α ennreal)  :
= ∫⁻ (a : α), f a μ
theorem measure_theory.ae_eq_fun.coe_fn_abs {α : Type u_1} {μ : measure_theory.measure α} {β : Type u_2} [lattice β] [add_group β] (f : α →ₘ[μ] β) :
|f| =ᵐ[μ] λ (x : α), |f x|
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 : α γ)  :
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 : α), linear_order.max (f a) 0
def continuous_map.to_ae_eq_fun {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) [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 α] (f : C(α, β)) :
def continuous_map.to_ae_eq_fun_add_hom {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) [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.

Equations
def continuous_map.to_ae_eq_fun_mul_hom {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) [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 𝕜] [ γ]  :
C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ

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

Equations