# Almost everywhere equal functions #

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 L1Space.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_toFun, neg_toFun, sub_toFun, smul_toFun

• 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.toFun : To find a representative of f : α →ₘ β, use the coercion (f : α → β), which is implemented as f.toFun. 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 [fun a ↦ g (f₁ a) (f₂ a)]. For example, [f + g] is comp₂ (+)

## Tags #

function space, almost everywhere equal, L⁰, ae_eq_fun

def MeasureTheory.Measure.aeEqSetoid {α : Type u_1} (β : Type u_2) [] [] (μ : ) :
Setoid { f : αβ // }

The equivalence relation of being almost everywhere equal for almost everywhere strongly measurable functions.

Equations
• = { r := fun (f g : { f : αβ // }) => f =ᵐ[μ] g, iseqv := }
Instances For
def MeasureTheory.AEEqFun (α : Type u_1) (β : Type u_2) [] [] (μ : ) :
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

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
• One or more equations did not get rendered due to their size.
Instances For
def MeasureTheory.AEEqFun.mk {α : Type u_1} [] {μ : } {β : Type u_5} [] (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
Instances For
def MeasureTheory.AEEqFun.cast {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
αβ

Coercion from a space of equivalence classes of almost everywhere strongly measurable functions to functions.

Equations
Instances For
instance MeasureTheory.AEEqFun.instCoeFun {α : Type u_1} {β : Type u_2} [] {μ : } [] :
CoeFun (α →ₘ[μ] β) fun (x : α →ₘ[μ] β) => αβ

A measurable representative of an AEEqFun [f]

Equations
• MeasureTheory.AEEqFun.instCoeFun = { coe := MeasureTheory.AEEqFun.cast }
theorem MeasureTheory.AEEqFun.stronglyMeasurable {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.measurable {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.aemeasurable {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) :
AEMeasurable (f) μ
@[simp]
theorem MeasureTheory.AEEqFun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : αβ) (hf : ) :
Quot.mk Setoid.r f, hf =
@[simp]
theorem MeasureTheory.AEEqFun.mk_eq_mk {α : Type u_1} {β : Type u_2} [] {μ : } [] {f : αβ} {g : αβ} {hf : } {hg : } :
f =ᵐ[μ] g
@[simp]
theorem MeasureTheory.AEEqFun.mk_coeFn {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.ext {α : Type u_1} {β : Type u_2} [] {μ : } [] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) :
f = g
theorem MeasureTheory.AEEqFun.ext_iff {α : Type u_1} {β : Type u_2} [] {μ : } [] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
f = g f =ᵐ[μ] g
theorem MeasureTheory.AEEqFun.coeFn_mk {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : αβ) (hf : ) :
() =ᵐ[μ] f
theorem MeasureTheory.AEEqFun.induction_on {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β)Prop} (H : ∀ (f : αβ) (hf : ), p ()) :
p f
theorem MeasureTheory.AEEqFun.induction_on₂ {α : Type u_1} {β : Type u_2} [] {μ : } [] {α' : Type u_5} {β' : Type u_6} [] [] {μ' : } (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β)(α' →ₘ[μ'] β')Prop} (H : ∀ (f : αβ) (hf : ) (f' : α'β') (hf' : ), p () ()) :
p f f'
theorem MeasureTheory.AEEqFun.induction_on₃ {α : Type u_1} {β : Type u_2} [] {μ : } [] {α' : Type u_5} {β' : Type u_6} [] [] {μ' : } {α'' : Type u_7} {β'' : Type u_8} [] [] {μ'' : } (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'') {p : (α →ₘ[μ] β)(α' →ₘ[μ'] β')(α'' →ₘ[μ''] β'')Prop} (H : ∀ (f : αβ) (hf : ) (f' : α'β') (hf' : ) (f'' : α''β'') (hf'' : ), p () () (MeasureTheory.AEEqFun.mk f'' hf'')) :
p f f' f''

### Composition of an a.e. equal function with a (quasi) measure preserving function #

def MeasureTheory.AEEqFun.compQuasiMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } (g : β →ₘ[ν] γ) (f : αβ) (hf : ) :
α →ₘ[μ] γ

Composition of an almost everywhere equal function and a quasi measure preserving function.

See also AEEqFun.compMeasurePreserving.

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} {g : βγ} (hg : ) (hf : ) :
().compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} (g : β →ₘ[ν] γ) (hf : ) :
g.compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
theorem MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} (g : β →ₘ[ν] γ) (hf : ) :
(g.compQuasiMeasurePreserving f hf) =ᵐ[μ] g f
def MeasureTheory.AEEqFun.compMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } (g : β →ₘ[ν] γ) (f : αβ) (hf : ) :
α →ₘ[μ] γ

Composition of an almost everywhere equal function and a quasi measure preserving function.

This is an important special case of AEEqFun.compQuasiMeasurePreserving. We use a separate definition so that lemmas that need f to be measure preserving can be @[simp] lemmas.

Equations
• g.compMeasurePreserving f hf = g.compQuasiMeasurePreserving f
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.compMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} {g : βγ} (hg : ) (hf : ) :
().compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
theorem MeasureTheory.AEEqFun.compMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} (g : β →ₘ[ν] γ) (hf : ) :
g.compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
theorem MeasureTheory.AEEqFun.coeFn_compMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {ν : } {f : αβ} (g : β →ₘ[ν] γ) (hf : ) :
(g.compMeasurePreserving f hf) =ᵐ[μ] g f
def MeasureTheory.AEEqFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (g : βγ) (hg : ) (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
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.comp_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (g : βγ) (hg : ) (f : αβ) (hf : ) :
theorem MeasureTheory.AEEqFun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.coeFn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
() =ᵐ[μ] g f
theorem MeasureTheory.AEEqFun.comp_compQuasiMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] {ν : } (g : γδ) (hg : ) (f : β →ₘ[ν] γ) {φ : αβ} (hφ : ) :
().compQuasiMeasurePreserving φ = MeasureTheory.AEEqFun.comp g hg (f.compQuasiMeasurePreserving φ )
def MeasureTheory.AEEqFun.compMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] [] [] [] (g : βγ) (hg : ) (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
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.compMeasurable_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] [] [] [] (g : βγ) (hg : ) (f : αβ) (hf : ) :
theorem MeasureTheory.AEEqFun.compMeasurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] [] [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
theorem MeasureTheory.AEEqFun.coeFn_compMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] [] [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
() =ᵐ[μ] g f
def MeasureTheory.AEEqFun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
α →ₘ[μ] β × γ

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.pair_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (f : αβ) (hf : ) (g : αγ) (hg : ) :
().pair () = MeasureTheory.AEEqFun.mk (fun (x : α) => (f x, g x))
theorem MeasureTheory.AEEqFun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
f.pair g = MeasureTheory.AEEqFun.mk (fun (x : α) => (f x, g x))
theorem MeasureTheory.AEEqFun.coeFn_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
(f.pair g) =ᵐ[μ] fun (x : α) => (f x, g x)
def MeasureTheory.AEEqFun.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
α →ₘ[μ] δ

Given a continuous function g : β → γ → δ, and almost everywhere equal functions [f₁] : α →ₘ β and [f₂] : α →ₘ γ, return the equivalence class of the function fun a => g (f₁ a) (f₂ a), i.e., the almost everywhere equal function [fun a => g (f₁ a) (f₂ a)] : α →ₘ γ

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.comp₂_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : αβ) (f₂ : αγ) (hf₁ : ) (hf₂ : ) :
MeasureTheory.AEEqFun.comp₂ g hg () () = MeasureTheory.AEEqFun.mk (fun (a : α) => g (f₁ a) (f₂ a))
theorem MeasureTheory.AEEqFun.comp₂_eq_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.comp () hg (f₁.pair f₂)
theorem MeasureTheory.AEEqFun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.mk (fun (a : α) => g (f₁ a) (f₂ a))
theorem MeasureTheory.AEEqFun.coeFn_comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂) =ᵐ[μ] fun (a : α) => g (f₁ a) (f₂ a)
def MeasureTheory.AEEqFun.comp₂Measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
α →ₘ[μ] δ

Given a measurable function g : β → γ → δ, and almost everywhere equal functions [f₁] : α →ₘ β and [f₂] : α →ₘ γ, return the equivalence class of the function fun a => g (f₁ a) (f₂ a), i.e., the almost everywhere equal function [fun a => g (f₁ a) (f₂ a)] : α →ₘ γ. This requires δ to have second-countable topology.

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.comp₂Measurable_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : αβ) (f₂ : αγ) (hf₁ : ) (hf₂ : ) :
= MeasureTheory.AEEqFun.mk (fun (a : α) => g (f₁ a) (f₂ a))
theorem MeasureTheory.AEEqFun.comp₂Measurable_eq_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
= MeasureTheory.AEEqFun.compMeasurable () hg (f₁.pair f₂)
theorem MeasureTheory.AEEqFun.comp₂Measurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
= MeasureTheory.AEEqFun.mk (fun (a : α) => g (f₁ a) (f₂ a))
theorem MeasureTheory.AEEqFun.coeFn_comp₂Measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
() =ᵐ[μ] fun (a : α) => g (f₁ a) (f₂ a)
def MeasureTheory.AEEqFun.toGerm {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
().Germ β

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

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.mk_toGerm {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : αβ) (hf : ) :
().toGerm = f
theorem MeasureTheory.AEEqFun.toGerm_eq {α : Type u_1} {β : Type u_2} [] {μ : } [] (f : α →ₘ[μ] β) :
f.toGerm = f
theorem MeasureTheory.AEEqFun.toGerm_injective {α : Type u_1} {β : Type u_2} [] {μ : } [] :
Function.Injective MeasureTheory.AEEqFun.toGerm
@[simp]
theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {f : αβ} {ν : } (g : β →ₘ[ν] γ) (hf : ) :
(g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f
@[simp]
theorem MeasureTheory.AEEqFun.compMeasurePreserving_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {f : αβ} {ν : } (g : β →ₘ[ν] γ) (hf : ) :
(g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f
theorem MeasureTheory.AEEqFun.comp_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
().toGerm = Filter.Germ.map g f.toGerm
theorem MeasureTheory.AEEqFun.compMeasurable_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] [] [] [] (g : βγ) (hg : ) (f : α →ₘ[μ] β) :
().toGerm = Filter.Germ.map g f.toGerm
theorem MeasureTheory.AEEqFun.comp₂_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
theorem MeasureTheory.AEEqFun.comp₂Measurable_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] {μ : } [] [] [] [] [] [] [] [] (g : βγδ) (hg : ) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
().toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
def MeasureTheory.AEEqFun.LiftPred {α : Type u_1} {β : Type u_2} [] {μ : } [] (p : βProp) (f : α →ₘ[μ] β) :

Given a predicate p and an equivalence class [f], return true if p holds of f a for almost all a

Equations
Instances For
def MeasureTheory.AEEqFun.LiftRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] (r : βγProp) (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :

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
Instances For
theorem MeasureTheory.AEEqFun.liftRel_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {r : βγProp} {f : αβ} {g : αγ} {hf : } {hg : } :
∀ᵐ (a : α) ∂μ, r (f a) (g a)
theorem MeasureTheory.AEEqFun.liftRel_iff_coeFn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {μ : } [] [] {r : βγProp} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
∀ᵐ (a : α) ∂μ, r (f a) (g a)
instance MeasureTheory.AEEqFun.instPreorder {α : Type u_1} {β : Type u_2} [] {μ : } [] [] :
Preorder (α →ₘ[μ] β)
Equations
• MeasureTheory.AEEqFun.instPreorder = Preorder.lift MeasureTheory.AEEqFun.toGerm
@[simp]
theorem MeasureTheory.AEEqFun.mk_le_mk {α : Type u_1} {β : Type u_2} [] {μ : } [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
f ≤ᵐ[μ] g
@[simp]
theorem MeasureTheory.AEEqFun.coeFn_le {α : Type u_1} {β : Type u_2} [] {μ : } [] [] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
f ≤ᵐ[μ] g f g
instance MeasureTheory.AEEqFun.instPartialOrder {α : Type u_1} {β : Type u_2} [] {μ : } [] [] :
Equations
• MeasureTheory.AEEqFun.instPartialOrder = PartialOrder.lift MeasureTheory.AEEqFun.toGerm
instance MeasureTheory.AEEqFun.instSup {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] :
Sup (α →ₘ[μ] β)
Equations
theorem MeasureTheory.AEEqFun.coeFn_sup {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] fun (x : α) => f x g x
theorem MeasureTheory.AEEqFun.le_sup_left {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
f f g
theorem MeasureTheory.AEEqFun.le_sup_right {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
g f g
theorem MeasureTheory.AEEqFun.sup_le {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) (f' : α →ₘ[μ] β) (hf : f f') (hg : g f') :
f g f'
instance MeasureTheory.AEEqFun.instInf {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] :
Inf (α →ₘ[μ] β)
Equations
theorem MeasureTheory.AEEqFun.coeFn_inf {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
(f g) =ᵐ[μ] fun (x : α) => f x g x
theorem MeasureTheory.AEEqFun.inf_le_left {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
f g f
theorem MeasureTheory.AEEqFun.inf_le_right {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
f g g
theorem MeasureTheory.AEEqFun.le_inf {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] (f' : α →ₘ[μ] β) (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) (hf : f' f) (hg : f' g) :
f' f g
instance MeasureTheory.AEEqFun.instLattice {α : Type u_1} {β : Type u_2} [] {μ : } [] [] :
Lattice (α →ₘ[μ] β)
Equations
• MeasureTheory.AEEqFun.instLattice = let __src := MeasureTheory.AEEqFun.instPartialOrder; Lattice.mk
def MeasureTheory.AEEqFun.const (α : Type u_1) {β : Type u_2} [] {μ : } [] (b : β) :
α →ₘ[μ] β

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

Equations
Instances For
theorem MeasureTheory.AEEqFun.coeFn_const (α : Type u_1) {β : Type u_2} [] {μ : } [] (b : β) :
=ᵐ[μ]
instance MeasureTheory.AEEqFun.instInhabited {α : Type u_1} {β : Type u_2} [] {μ : } [] [] :
Equations
instance MeasureTheory.AEEqFun.instZero {α : Type u_1} {β : Type u_2} [] {μ : } [] [Zero β] :
Zero (α →ₘ[μ] β)
Equations
• MeasureTheory.AEEqFun.instZero = { zero := }
instance MeasureTheory.AEEqFun.instOne {α : Type u_1} {β : Type u_2} [] {μ : } [] [One β] :
One (α →ₘ[μ] β)
Equations
• MeasureTheory.AEEqFun.instOne = { one := }
theorem MeasureTheory.AEEqFun.zero_def {α : Type u_1} {β : Type u_2} [] {μ : } [] [Zero β] :
0 = MeasureTheory.AEEqFun.mk (fun (x : α) => 0)
theorem MeasureTheory.AEEqFun.one_def {α : Type u_1} {β : Type u_2} [] {μ : } [] [One β] :
1 = MeasureTheory.AEEqFun.mk (fun (x : α) => 1)
theorem MeasureTheory.AEEqFun.coeFn_zero {α : Type u_1} {β : Type u_2} [] {μ : } [] [Zero β] :
0 =ᵐ[μ] 0
theorem MeasureTheory.AEEqFun.coeFn_one {α : Type u_1} {β : Type u_2} [] {μ : } [] [One β] :
1 =ᵐ[μ] 1
@[simp]
theorem MeasureTheory.AEEqFun.zero_toGerm {α : Type u_1} {β : Type u_2} [] {μ : } [] [Zero β] :
@[simp]
theorem MeasureTheory.AEEqFun.one_toGerm {α : Type u_1} {β : Type u_2} [] {μ : } [] [One β] :
instance MeasureTheory.AEEqFun.instSMul {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [SMul 𝕜 γ] [] :
SMul 𝕜 (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.smul_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [SMul 𝕜 γ] [] (c : 𝕜) (f : αγ) (hf : ) :
theorem MeasureTheory.AEEqFun.coeFn_smul {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [SMul 𝕜 γ] [] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f) =ᵐ[μ] c f
theorem MeasureTheory.AEEqFun.smul_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [SMul 𝕜 γ] [] (c : 𝕜) (f : α →ₘ[μ] γ) :
(c f).toGerm = c f.toGerm
instance MeasureTheory.AEEqFun.instSMulCommClass {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} {𝕜' : Type u_6} [SMul 𝕜 γ] [] [SMul 𝕜' γ] [] [SMulCommClass 𝕜 𝕜' γ] :
SMulCommClass 𝕜 𝕜' (α →ₘ[μ] γ)
Equations
• =
instance MeasureTheory.AEEqFun.instIsScalarTower {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} {𝕜' : Type u_6} [SMul 𝕜 γ] [] [SMul 𝕜' γ] [] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' γ] :
IsScalarTower 𝕜 𝕜' (α →ₘ[μ] γ)
Equations
• =
instance MeasureTheory.AEEqFun.instIsCentralScalar {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [SMul 𝕜 γ] [] [SMul 𝕜ᵐᵒᵖ γ] [] :
IsCentralScalar 𝕜 (α →ₘ[μ] γ)
Equations
• =
instance MeasureTheory.AEEqFun.instAdd {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Add γ] [] :
Equations
instance MeasureTheory.AEEqFun.instMul {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Mul γ] [] :
Mul (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.mk_add_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Add γ] [] (f : αγ) (g : αγ) (hf : ) (hg : ) :
@[simp]
theorem MeasureTheory.AEEqFun.mk_mul_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Mul γ] [] (f : αγ) (g : αγ) (hf : ) (hg : ) :
theorem MeasureTheory.AEEqFun.coeFn_add {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Add γ] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f + g) =ᵐ[μ] f + g
theorem MeasureTheory.AEEqFun.coeFn_mul {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Mul γ] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f * g) =ᵐ[μ] f * g
@[simp]
theorem MeasureTheory.AEEqFun.add_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Add γ] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f + g).toGerm = f.toGerm + g.toGerm
@[simp]
theorem MeasureTheory.AEEqFun.mul_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [Mul γ] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f * g).toGerm = f.toGerm * g.toGerm
instance MeasureTheory.AEEqFun.instAddMonoid {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Equations
instance MeasureTheory.AEEqFun.instAddCommMonoid {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Equations
instance MeasureTheory.AEEqFun.instPowNat {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Pow (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.mk_pow {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : αγ) (hf : ) (n : ) :
theorem MeasureTheory.AEEqFun.coeFn_pow {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem MeasureTheory.AEEqFun.pow_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).toGerm = f.toGerm ^ n
instance MeasureTheory.AEEqFun.instMonoid {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Monoid (α →ₘ[μ] γ)
Equations
def MeasureTheory.AEEqFun.toGermAddMonoidHom {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
(α →ₘ[μ] γ) →+ ().Germ γ

AEEqFun.toGerm as an AddMonoidHom.

Equations
• MeasureTheory.AEEqFun.toGermAddMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_zero' := , map_add' := }
Instances For
theorem MeasureTheory.AEEqFun.toGermAddMonoidHom.proof_2 {α : Type u_2} {γ : Type u_1} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f + g).toGerm = f.toGerm + g.toGerm
theorem MeasureTheory.AEEqFun.toGermAddMonoidHom.proof_1 {α : Type u_1} {γ : Type u_2} [] {μ : } [] [] :
@[simp]
theorem MeasureTheory.AEEqFun.toGermMonoidHom_apply {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) :
MeasureTheory.AEEqFun.toGermMonoidHom f = f.toGerm
@[simp]
theorem MeasureTheory.AEEqFun.toGermAddMonoidHom_apply {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) :
def MeasureTheory.AEEqFun.toGermMonoidHom {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
(α →ₘ[μ] γ) →* ().Germ γ

AEEqFun.toGerm as a MonoidHom.

Equations
• MeasureTheory.AEEqFun.toGermMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_one' := , map_mul' := }
Instances For
instance MeasureTheory.AEEqFun.instCommMonoid {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Equations
instance MeasureTheory.AEEqFun.instNeg {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] :
Neg (α →ₘ[μ] γ)
Equations
theorem MeasureTheory.AEEqFun.instNeg.proof_1 {γ : Type u_1} [] [] :
Continuous fun (a : γ) => -a
instance MeasureTheory.AEEqFun.instInv {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Inv (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.neg_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : αγ) (hf : ) :
@[simp]
theorem MeasureTheory.AEEqFun.inv_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : αγ) (hf : ) :
theorem MeasureTheory.AEEqFun.coeFn_neg {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] γ) :
(-f) =ᵐ[μ] -f
theorem MeasureTheory.AEEqFun.coeFn_inv {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) :
f⁻¹ =ᵐ[μ] (f)⁻¹
theorem MeasureTheory.AEEqFun.neg_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] γ) :
(-f).toGerm = -f.toGerm
theorem MeasureTheory.AEEqFun.inv_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) :
f⁻¹.toGerm = f.toGerm⁻¹
instance MeasureTheory.AEEqFun.instSub {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] :
Sub (α →ₘ[μ] γ)
Equations
theorem MeasureTheory.AEEqFun.instSub.proof_1 {γ : Type u_1} [] [] :
Continuous fun (p : γ × γ) => p.1 - p.2
instance MeasureTheory.AEEqFun.instDiv {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Div (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.mk_sub {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : αγ) (g : αγ) (hf : ) (hg : ) :
@[simp]
theorem MeasureTheory.AEEqFun.mk_div {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : αγ) (g : αγ) (hf : ) (hg : ) :
theorem MeasureTheory.AEEqFun.coeFn_sub {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f - g) =ᵐ[μ] f - g
theorem MeasureTheory.AEEqFun.coeFn_div {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f / g) =ᵐ[μ] f / g
theorem MeasureTheory.AEEqFun.sub_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f - g).toGerm = f.toGerm - g.toGerm
theorem MeasureTheory.AEEqFun.div_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
(f / g).toGerm = f.toGerm / g.toGerm
instance MeasureTheory.AEEqFun.instPowInt {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Pow (α →ₘ[μ] γ)
Equations
@[simp]
theorem MeasureTheory.AEEqFun.mk_zpow {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : αγ) (hf : ) (n : ) :
theorem MeasureTheory.AEEqFun.coeFn_zpow {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n) =ᵐ[μ] f ^ n
@[simp]
theorem MeasureTheory.AEEqFun.zpow_toGerm {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] (f : α →ₘ[μ] γ) (n : ) :
(f ^ n).toGerm = f.toGerm ^ n
instance MeasureTheory.AEEqFun.instAddGroup {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] :
Equations
instance MeasureTheory.AEEqFun.instAddCommGroup {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] :
Equations
instance MeasureTheory.AEEqFun.instGroup {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Group (α →ₘ[μ] γ)
Equations
instance MeasureTheory.AEEqFun.instCommGroup {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [] :
Equations
• MeasureTheory.AEEqFun.instCommGroup =
instance MeasureTheory.AEEqFun.instMulAction {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [] [] [] :
MulAction 𝕜 (α →ₘ[μ] γ)
Equations
instance MeasureTheory.AEEqFun.instDistribMulAction {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [] [] [] [] [] :
DistribMulAction 𝕜 (α →ₘ[μ] γ)
Equations
instance MeasureTheory.AEEqFun.instModule {α : Type u_1} {γ : Type u_3} [] {μ : } [] {𝕜 : Type u_5} [] [] [] [Module 𝕜 γ] [] :
Module 𝕜 (α →ₘ[μ] γ)
Equations
def MeasureTheory.AEEqFun.lintegral {α : Type u_1} [] {μ : } (f : ) :

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

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.lintegral_mk {α : Type u_1} [] {μ : } (f : αENNReal) (hf : ) :
().lintegral = ∫⁻ (a : α), f aμ
theorem MeasureTheory.AEEqFun.lintegral_coeFn {α : Type u_1} [] {μ : } (f : ) :
∫⁻ (a : α), f aμ = f.lintegral
@[simp]
theorem MeasureTheory.AEEqFun.lintegral_zero {α : Type u_1} [] {μ : } :
@[simp]
theorem MeasureTheory.AEEqFun.lintegral_eq_zero_iff {α : Type u_1} [] {μ : } {f : } :
f.lintegral = 0 f = 0
theorem MeasureTheory.AEEqFun.lintegral_add {α : Type u_1} [] {μ : } (f : ) (g : ) :
(f + g).lintegral = f.lintegral + g.lintegral
theorem MeasureTheory.AEEqFun.lintegral_mono {α : Type u_1} [] {μ : } {f : } {g : } :
f gf.lintegral g.lintegral
theorem MeasureTheory.AEEqFun.coeFn_abs {α : Type u_1} [] {μ : } {β : Type u_5} [] [] [] (f : α →ₘ[μ] β) :
|f| =ᵐ[μ] fun (x : α) => |f x|
def MeasureTheory.AEEqFun.posPart {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [Zero γ] (f : α →ₘ[μ] γ) :
α →ₘ[μ] γ

Positive part of an AEEqFun.

Equations
Instances For
@[simp]
theorem MeasureTheory.AEEqFun.posPart_mk {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [Zero γ] (f : αγ) (hf : ) :
().posPart = MeasureTheory.AEEqFun.mk (fun (x : α) => max (f x) 0)
theorem MeasureTheory.AEEqFun.coeFn_posPart {α : Type u_1} {γ : Type u_3} [] {μ : } [] [] [Zero γ] (f : α →ₘ[μ] γ) :
f.posPart =ᵐ[μ] fun (a : α) => max (f a) 0
def ContinuousMap.toAEEqFun {α : Type u_1} {β : Type u_2} [] (μ : ) [] [] [] (f : C(α, β)) :
α →ₘ[μ] β

The equivalence class of μ-almost-everywhere measurable functions associated to a continuous map.

Equations
Instances For
theorem ContinuousMap.coeFn_toAEEqFun {α : Type u_1} {β : Type u_2} [] (μ : ) [] [] [] (f : C(α, β)) :
() =ᵐ[μ] f
def ContinuousMap.toAEEqFunAddHom {α : Type u_1} {β : Type u_2} [] (μ : ) [] [] [] [] :
C(α, β) →+ α →ₘ[μ] β

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

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
theorem ContinuousMap.toAEEqFunAddHom.proof_2 {α : Type u_2} {β : Type u_1} [] (μ : ) [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
= MeasureTheory.AEEqFun.mk (f + g)
theorem ContinuousMap.toAEEqFunAddHom.proof_1 {α : Type u_1} {β : Type u_2} [] (μ : ) [] [] [] [] :
def ContinuousMap.toAEEqFunMulHom {α : Type u_1} {β : Type u_2} [] (μ : ) [] [] [] [] [] :
C(α, β) →* α →ₘ[μ] β

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

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
def ContinuousMap.toAEEqFunLinearMap {α : Type u_1} {γ : Type u_3} [] (μ : ) [] [] {𝕜 : Type u_5} [] [] [] [Module 𝕜 γ] [] :
C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ

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

Equations
• = let __src := ; { toFun := (__src).toFun, map_add' := , map_smul' := }
Instances For