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 Mathlib/MeasureTheory/Function/L1Space/AEEqFun.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, smul_mk, coeFn_add, coeFn_neg, coeFn_sub, coeFn_smul

• 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.cast: 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 : α → β).
• AEEqFun.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 compMeasurable 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) [MeasurableSpace α] [TopologicalSpace β] (μ : Measure α) : Setoid { f : α → β // AEStronglyMeasurable f μ }

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

def MeasureTheory.AEEqFun (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [TopologicalSpace β] (μ : 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.

def MeasureTheory.«term_→ₘ[_]_» : Lean.TrailingParserDescr

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.

def MeasureTheory.AEEqFun.mk {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {β : Type u_5} [TopologicalSpace β] (f : α → β) (hf : AEStronglyMeasurable f μ) : α →ₘ[μ] β

Construct the equivalence class [f] of an almost everywhere measurable function f, based on the equivalence relation of being almost everywhere equal.

def MeasureTheory.AEEqFun.cast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : α → β

Coercion from a space of equivalence classes of almost everywhere strongly measurable functions to functions. We ensure that if f has a constant representative, then we choose that one.

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

A measurable representative of an AEEqFun [f]

theorem MeasureTheory.AEEqFun.stronglyMeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : StronglyMeasurable ↑f

theorem MeasureTheory.AEEqFun.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : AEStronglyMeasurable (↑f) μ

theorem MeasureTheory.AEEqFun.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (f : α →ₘ[μ] β) : Measurable ↑f

theorem MeasureTheory.AEEqFun.aemeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (f : α →ₘ[μ] β) : AEMeasurable (↑f) μ

@[simp]

theorem MeasureTheory.AEEqFun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α → β) (hf : AEStronglyMeasurable f μ) : Quot.mk ⇑(Measure.aeEqSetoid β μ) ⟨f, hf⟩ = mk f hf

@[simp]

theorem MeasureTheory.AEEqFun.mk_eq_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {f g : α → β} {hf : AEStronglyMeasurable f μ} {hg : AEStronglyMeasurable g μ} : mk f hf = mk g hg ↔ f =ᶠ[ae μ] g

@[simp]

theorem MeasureTheory.AEEqFun.mk_coeFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : mk ↑f ⋯ = f

theorem MeasureTheory.AEEqFun.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {f g : α →ₘ[μ] β} (h : ↑f =ᶠ[ae μ] ↑g) : f = g

theorem MeasureTheory.AEEqFun.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {f g : α →ₘ[μ] β} : f = g ↔ ↑f =ᶠ[ae μ] ↑g

theorem MeasureTheory.AEEqFun.coeFn_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α → β) (hf : AEStronglyMeasurable f μ) : ↑(mk f hf) =ᶠ[ae μ] f

theorem MeasureTheory.AEEqFun.induction_on {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop} (H : ∀ (f : α → β) (hf : AEStronglyMeasurable f μ), p (mk f hf)) : p f

theorem MeasureTheory.AEEqFun.induction_on₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {α' : Type u_5} {β' : Type u_6} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : Measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop} (H : ∀ (f : α → β) (hf : AEStronglyMeasurable f μ) (f' : α' → β') (hf' : AEStronglyMeasurable f' μ'), p (mk f hf) (mk f' hf')) : p f f'

theorem MeasureTheory.AEEqFun.induction_on₃ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {α' : Type u_5} {β' : Type u_6} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : Measure α'} {α'' : Type u_7} {β'' : Type u_8} [MeasurableSpace α''] [TopologicalSpace β''] {μ'' : Measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop} (H : ∀ (f : α → β) (hf : AEStronglyMeasurable f μ) (f' : α' → β') (hf' : AEStronglyMeasurable f' μ') (f'' : α'' → β'') (hf'' : AEStronglyMeasurable f'' μ''), p (mk f hf) (mk f' hf') (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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} (g : β →ₘ[ν] γ) (f : α → β) (hf : Measure.QuasiMeasurePreserving f μ ν) : α →ₘ[μ] γ

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

See also AEEqFun.compMeasurePreserving.

@[simp]

theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} {g : β → γ} (hg : AEStronglyMeasurable g ν) (hf : Measure.QuasiMeasurePreserving f μ ν) : (mk g hg).compQuasiMeasurePreserving f hf = mk (g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} (g : β →ₘ[ν] γ) (hf : Measure.QuasiMeasurePreserving f μ ν) : g.compQuasiMeasurePreserving f hf = mk (↑g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} (g : β →ₘ[ν] γ) (hf : Measure.QuasiMeasurePreserving f μ ν) : ↑(g.compQuasiMeasurePreserving f hf) =ᶠ[ae μ] ↑g ∘ f

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

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.

@[simp]

theorem MeasureTheory.AEEqFun.compMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} {g : β → γ} (hg : AEStronglyMeasurable g ν) (hf : MeasurePreserving f μ ν) : (mk g hg).compMeasurePreserving f hf = mk (g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.compMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} (g : β →ₘ[ν] γ) (hf : MeasurePreserving f μ ν) : g.compMeasurePreserving f hf = mk (↑g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_compMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : Measure β} {f : α → β} (g : β →ₘ[ν] γ) (hf : MeasurePreserving f μ ν) : ↑(g.compMeasurePreserving f hf) =ᶠ[ae μ] ↑g ∘ f

def MeasureTheory.AEEqFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (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] : α →ₘ γ.

@[simp]

theorem MeasureTheory.AEEqFun.comp_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α → β) (hf : AEStronglyMeasurable f μ) : comp g hg (mk f hf) = mk (g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) : comp g hg f = mk (g ∘ ↑f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) : ↑(comp g hg f) =ᶠ[ae μ] g ∘ ↑f

theorem MeasureTheory.AEEqFun.comp_compQuasiMeasurePreserving {α : Type u_1} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace γ] {β : Type u_5} [MeasurableSpace β] {ν : Measure β} (g : γ → δ) (hg : Continuous g) (f : β →ₘ[ν] γ) {φ : α → β} (hφ : Measure.QuasiMeasurePreserving φ μ ν) : (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)

def MeasureTheory.AEEqFun.compMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (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.

@[simp]

theorem MeasureTheory.AEEqFun.compMeasurable_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α → β) (hf : AEStronglyMeasurable f μ) : compMeasurable g hg (mk f hf) = mk (g ∘ f) ⋯

theorem MeasureTheory.AEEqFun.compMeasurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) : compMeasurable g hg f = mk (g ∘ ↑f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_compMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) : ↑(compMeasurable g hg f) =ᶠ[ae μ] g ∘ ↑f

def MeasureTheory.AEEqFun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : α →ₘ[μ] β × γ

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

@[simp]

theorem MeasureTheory.AEEqFun.pair_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α → β) (hf : AEStronglyMeasurable f μ) (g : α → γ) (hg : AEStronglyMeasurable g μ) : (mk f hf).pair (mk g hg) = mk (fun (x : α) => (f x, g x)) ⋯

theorem MeasureTheory.AEEqFun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g = mk (fun (x : α) => (↑f x, ↑g x)) ⋯

theorem MeasureTheory.AEEqFun.coeFn_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : ↑(f.pair g) =ᶠ[ae μ] fun (x : α) => (↑f x, ↑g x)

def MeasureTheory.AEEqFun.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (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)] : α →ₘ γ

@[simp]

theorem MeasureTheory.AEEqFun.comp₂_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ : AEStronglyMeasurable f₁ μ) (hf₂ : AEStronglyMeasurable f₂ μ) : comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) = 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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : comp₂ g hg f₁ f₂ = comp (Function.uncurry g) hg (f₁.pair f₂)

theorem MeasureTheory.AEEqFun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : comp₂ g hg f₁ f₂ = 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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : ↑(comp₂ g hg f₁ f₂) =ᶠ[ae μ] fun (a : α) => g (↑f₁ a) (↑f₂ a)

def MeasureTheory.AEEqFun.comp₂Measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace δ] [TopologicalSpace.PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ] (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 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.

@[simp]

theorem MeasureTheory.AEEqFun.comp₂Measurable_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace δ] [TopologicalSpace.PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ : AEStronglyMeasurable f₁ μ) (hf₂ : AEStronglyMeasurable f₂ μ) : comp₂Measurable g hg (mk f₁ hf₁) (mk f₂ hf₂) = 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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace δ] [TopologicalSpace.PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : comp₂Measurable g hg f₁ f₂ = compMeasurable (Function.uncurry g) hg (f₁.pair f₂)

theorem MeasureTheory.AEEqFun.comp₂Measurable_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace δ] [TopologicalSpace.PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : comp₂Measurable g hg f₁ f₂ = 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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [MeasurableSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace δ] [TopologicalSpace.PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : ↑(comp₂Measurable g hg f₁ f₂) =ᶠ[ae μ] fun (a : α) => g (↑f₁ a) (↑f₂ a)

def MeasureTheory.AEEqFun.toGerm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : (ae μ).Germ β

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

@[simp]

theorem MeasureTheory.AEEqFun.mk_toGerm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α → β) (hf : AEStronglyMeasurable f μ) : (mk f hf).toGerm = ↑f

theorem MeasureTheory.AEEqFun.toGerm_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) : f.toGerm = ↑↑f

theorem MeasureTheory.AEEqFun.toGerm_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] : Function.Injective toGerm

@[simp]

theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {β : Type u_5} [MeasurableSpace β] {f : α → β} {ν : Measure β} (g : β →ₘ[ν] γ) (hf : Measure.QuasiMeasurePreserving f μ ν) : (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

@[simp]

theorem MeasureTheory.AEEqFun.compMeasurePreserving_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {β : Type u_5} [MeasurableSpace β] {f : α → β} {ν : Measure β} (g : β →ₘ[ν] γ) (hf : MeasurePreserving f μ ν) : (g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

theorem MeasureTheory.AEEqFun.comp_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) : (comp g hg f).toGerm = Filter.Germ.map g f.toGerm

theorem MeasureTheory.AEEqFun.compMeasurable_toGerm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] [MeasurableSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [TopologicalSpace.PseudoMetrizableSpace γ] [SecondCountableTopology γ] [MeasurableSpace γ] [OpensMeasurableSpace γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) : (compMeasurable 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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : (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} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace γ] [SecondCountableTopologyEither β γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace.PseudoMetrizableSpace δ] [SecondCountableTopology δ] [MeasurableSpace δ] [OpensMeasurableSpace δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : (comp₂Measurable g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm

def MeasureTheory.AEEqFun.LiftPred {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (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

def MeasureTheory.AEEqFun.LiftRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] (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

theorem MeasureTheory.AEEqFun.liftRel_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf : AEStronglyMeasurable f μ} {hg : AEStronglyMeasurable g μ} : LiftRel r (mk f hf) (mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (f a) (g a)

theorem MeasureTheory.AEEqFun.liftRel_iff_coeFn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ] {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} : LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (↑f a) (↑g a)

instance MeasureTheory.AEEqFun.instPreorder {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Preorder β] : Preorder (α →ₘ[μ] β)

@[simp]

theorem MeasureTheory.AEEqFun.mk_le_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Preorder β] {f g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : mk f hf ≤ mk g hg ↔ f ≤ᶠ[ae μ] g

@[simp]

theorem MeasureTheory.AEEqFun.coeFn_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Preorder β] {f g : α →ₘ[μ] β} : ↑f ≤ᶠ[ae μ] ↑g ↔ f ≤ g

instance MeasureTheory.AEEqFun.instPartialOrder {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [PartialOrder β] : PartialOrder (α →ₘ[μ] β)

instance MeasureTheory.AEEqFun.instSup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] : Max (α →ₘ[μ] β)

theorem MeasureTheory.AEEqFun.coeFn_sup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f g : α →ₘ[μ] β) : ↑(f ⊔ g) =ᶠ[ae μ] fun (x : α) => ↑f x ⊔ ↑g x

theorem MeasureTheory.AEEqFun.le_sup_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f g : α →ₘ[μ] β) : f ≤ f ⊔ g

theorem MeasureTheory.AEEqFun.le_sup_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f g : α →ₘ[μ] β) : g ≤ f ⊔ g

theorem MeasureTheory.AEEqFun.sup_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f'

instance MeasureTheory.AEEqFun.instInf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] : Min (α →ₘ[μ] β)

theorem MeasureTheory.AEEqFun.coeFn_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f g : α →ₘ[μ] β) : ↑(f ⊓ g) =ᶠ[ae μ] fun (x : α) => ↑f x ⊓ ↑g x

theorem MeasureTheory.AEEqFun.inf_le_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f g : α →ₘ[μ] β) : f ⊓ g ≤ f

theorem MeasureTheory.AEEqFun.inf_le_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f g : α →ₘ[μ] β) : f ⊓ g ≤ g

theorem MeasureTheory.AEEqFun.le_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f' f g : α →ₘ[μ] β) (hf : f' ≤ f) (hg : f' ≤ g) : f' ≤ f ⊓ g

instance MeasureTheory.AEEqFun.instLattice {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Lattice β] [TopologicalLattice β] : Lattice (α →ₘ[μ] β)

def MeasureTheory.AEEqFun.const (α : Type u_1) {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (b : β) : α →ₘ[μ] β

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

theorem MeasureTheory.AEEqFun.coeFn_const (α : Type u_1) {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] (b : β) : ↑(const α b) =ᶠ[ae μ] Function.const α b

@[simp]

theorem MeasureTheory.AEEqFun.coeFn_const_eq (α : Type u_1) {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [NeZero μ] (b : β) (x : α) : ↑(const α b) x = b

If the measure is nonzero, we can strengthen coeFn_const to get an equality.

instance MeasureTheory.AEEqFun.instInhabited {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Inhabited β] : Inhabited (α →ₘ[μ] β)

instance MeasureTheory.AEEqFun.instOne {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [One β] : One (α →ₘ[μ] β)

instance MeasureTheory.AEEqFun.instZero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Zero β] : Zero (α →ₘ[μ] β)

theorem MeasureTheory.AEEqFun.one_def {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [One β] : 1 = mk (fun (x : α) => 1) ⋯

theorem MeasureTheory.AEEqFun.zero_def {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Zero β] : 0 = mk (fun (x : α) => 0) ⋯

theorem MeasureTheory.AEEqFun.coeFn_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [One β] : ↑1 =ᶠ[ae μ] 1

theorem MeasureTheory.AEEqFun.coeFn_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Zero β] : ↑0 =ᶠ[ae μ] 0

@[simp]

theorem MeasureTheory.AEEqFun.coeFn_one_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [NeZero μ] [One β] {x : α} : ↑1 x = 1

@[simp]

theorem MeasureTheory.AEEqFun.coeFn_zero_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [NeZero μ] [Zero β] {x : α} : ↑0 x = 0

@[simp]

theorem MeasureTheory.AEEqFun.one_toGerm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [One β] : toGerm 1 = 1

@[simp]

theorem MeasureTheory.AEEqFun.zero_toGerm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] [Zero β] : toGerm 0 = 0

instance MeasureTheory.AEEqFun.instSMul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : SMul 𝕜 (α →ₘ[μ] γ)

@[simp]

theorem MeasureTheory.AEEqFun.smul_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α → γ) (hf : AEStronglyMeasurable f μ) : c • mk f hf = mk (c • f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_smul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) : ↑(c • f) =ᶠ[ae μ] c • ↑f

theorem MeasureTheory.AEEqFun.smul_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) : (c • f).toGerm = c • f.toGerm

instance MeasureTheory.AEEqFun.instSMulCommClass {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} {𝕜' : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜' γ] [ContinuousConstSMul 𝕜' γ] [SMulCommClass 𝕜 𝕜' γ] : SMulCommClass 𝕜 𝕜' (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instIsScalarTower {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} {𝕜' : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜' γ] [ContinuousConstSMul 𝕜' γ] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' γ] : IsScalarTower 𝕜 𝕜' (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instIsCentralScalar {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜ᵐᵒᵖ γ] [IsCentralScalar 𝕜 γ] : IsCentralScalar 𝕜 (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instMul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] : Mul (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instAdd {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] : Add (α →ₘ[μ] γ)

@[simp]

theorem MeasureTheory.AEEqFun.mk_mul_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : mk f hf * mk g hg = mk (f * g) ⋯

@[simp]

theorem MeasureTheory.AEEqFun.mk_add_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : mk f hf + mk g hg = mk (f + g) ⋯

theorem MeasureTheory.AEEqFun.coeFn_mul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : α →ₘ[μ] γ) : ↑(f * g) =ᶠ[ae μ] ↑f * ↑g

theorem MeasureTheory.AEEqFun.coeFn_add {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : α →ₘ[μ] γ) : ↑(f + g) =ᶠ[ae μ] ↑f + ↑g

@[simp]

theorem MeasureTheory.AEEqFun.mul_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : α →ₘ[μ] γ) : (f * g).toGerm = f.toGerm * g.toGerm

@[simp]

theorem MeasureTheory.AEEqFun.add_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : α →ₘ[μ] γ) : (f + g).toGerm = f.toGerm + g.toGerm

instance MeasureTheory.AEEqFun.instAddMonoid {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] : AddMonoid (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instAddCommMonoid {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddCommMonoid γ] [ContinuousAdd γ] : AddCommMonoid (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instPowNat {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : Pow (α →ₘ[μ] γ) ℕ

@[simp]

theorem MeasureTheory.AEEqFun.mk_pow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α → γ) (hf : AEStronglyMeasurable f μ) (n : ℕ) : mk f hf ^ n = mk (f ^ n) ⋯

theorem MeasureTheory.AEEqFun.coeFn_pow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ℕ) : ↑(f ^ n) =ᶠ[ae μ] ↑f ^ n

@[simp]

theorem MeasureTheory.AEEqFun.pow_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ℕ) : (f ^ n).toGerm = f.toGerm ^ n

instance MeasureTheory.AEEqFun.instMonoid {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : Monoid (α →ₘ[μ] γ)

def MeasureTheory.AEEqFun.toGermMonoidHom {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : (α →ₘ[μ] γ) →* (ae μ).Germ γ

AEEqFun.toGerm as a MonoidHom.

def MeasureTheory.AEEqFun.toGermAddMonoidHom {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] : (α →ₘ[μ] γ) →+ (ae μ).Germ γ

AEEqFun.toGerm as an AddMonoidHom.

@[simp]

theorem MeasureTheory.AEEqFun.toGermAddMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) : toGermAddMonoidHom f = f.toGerm

@[simp]

theorem MeasureTheory.AEEqFun.toGermMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) : toGermMonoidHom f = f.toGerm

instance MeasureTheory.AEEqFun.instCommMonoid {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [CommMonoid γ] [ContinuousMul γ] : CommMonoid (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instInv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Inv (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instNeg {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : Neg (α →ₘ[μ] γ)

@[simp]

theorem MeasureTheory.AEEqFun.inv_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α → γ) (hf : AEStronglyMeasurable f μ) : (mk f hf)⁻¹ = mk f⁻¹ ⋯

@[simp]

theorem MeasureTheory.AEEqFun.neg_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : α → γ) (hf : AEStronglyMeasurable f μ) : -mk f hf = mk (-f) ⋯

theorem MeasureTheory.AEEqFun.coeFn_inv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₘ[μ] γ) : ↑f⁻¹ =ᶠ[ae μ] (↑f)⁻¹

theorem MeasureTheory.AEEqFun.coeFn_neg {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : α →ₘ[μ] γ) : ↑(-f) =ᶠ[ae μ] -↑f

theorem MeasureTheory.AEEqFun.inv_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₘ[μ] γ) : f⁻¹.toGerm = f.toGerm⁻¹

theorem MeasureTheory.AEEqFun.neg_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : α →ₘ[μ] γ) : (-f).toGerm = -f.toGerm

instance MeasureTheory.AEEqFun.instDiv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Div (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instSub {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : Sub (α →ₘ[μ] γ)

@[simp]

theorem MeasureTheory.AEEqFun.mk_div {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : mk (f / g) ⋯ = mk f hf / mk g hg

@[simp]

theorem MeasureTheory.AEEqFun.mk_sub {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : mk (f - g) ⋯ = mk f hf - mk g hg

theorem MeasureTheory.AEEqFun.coeFn_div {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : α →ₘ[μ] γ) : ↑(f / g) =ᶠ[ae μ] ↑f / ↑g

theorem MeasureTheory.AEEqFun.coeFn_sub {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : α →ₘ[μ] γ) : ↑(f - g) =ᶠ[ae μ] ↑f - ↑g

theorem MeasureTheory.AEEqFun.div_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : α →ₘ[μ] γ) : (f / g).toGerm = f.toGerm / g.toGerm

theorem MeasureTheory.AEEqFun.sub_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : α →ₘ[μ] γ) : (f - g).toGerm = f.toGerm - g.toGerm

instance MeasureTheory.AEEqFun.instPowInt {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Pow (α →ₘ[μ] γ) ℤ

@[simp]

theorem MeasureTheory.AEEqFun.mk_zpow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α → γ) (hf : AEStronglyMeasurable f μ) (n : ℤ) : mk f hf ^ n = mk (f ^ n) ⋯

theorem MeasureTheory.AEEqFun.coeFn_zpow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ℤ) : ↑(f ^ n) =ᶠ[ae μ] ↑f ^ n

@[simp]

theorem MeasureTheory.AEEqFun.zpow_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ℤ) : (f ^ n).toGerm = f.toGerm ^ n

instance MeasureTheory.AEEqFun.instAddGroup {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : AddGroup (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instAddCommGroup {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddCommGroup γ] [IsTopologicalAddGroup γ] : AddCommGroup (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instGroup {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Group (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instCommGroup {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [CommGroup γ] [IsTopologicalGroup γ] : CommGroup (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instMulAction {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Monoid 𝕜] [MulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : MulAction 𝕜 (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instDistribMulAction {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Monoid 𝕜] [AddMonoid γ] [ContinuousAdd γ] [DistribMulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : DistribMulAction 𝕜 (α →ₘ[μ] γ)

instance MeasureTheory.AEEqFun.instModule {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Semiring 𝕜] [AddCommMonoid γ] [ContinuousAdd γ] [Module 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : Module 𝕜 (α →ₘ[μ] γ)

def MeasureTheory.AEEqFun.lintegral {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f : α →ₘ[μ] ENNReal) : ENNReal

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

@[simp]

theorem MeasureTheory.AEEqFun.lintegral_mk {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f : α → ENNReal) (hf : AEStronglyMeasurable f μ) : (mk f hf).lintegral = ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.AEEqFun.lintegral_coeFn {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f : α →ₘ[μ] ENNReal) : ∫⁻ (a : α), ↑f a ∂μ = f.lintegral

@[simp]

theorem MeasureTheory.AEEqFun.lintegral_zero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} : lintegral 0 = 0

@[simp]

theorem MeasureTheory.AEEqFun.lintegral_eq_zero_iff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α →ₘ[μ] ENNReal} : f.lintegral = 0 ↔ f = 0

theorem MeasureTheory.AEEqFun.lintegral_add {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f g : α →ₘ[μ] ENNReal) : (f + g).lintegral = f.lintegral + g.lintegral

theorem MeasureTheory.AEEqFun.lintegral_mono {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f g : α →ₘ[μ] ENNReal} : f ≤ g → f.lintegral ≤ g.lintegral

theorem MeasureTheory.AEEqFun.coeFn_abs {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {β : Type u_5} [TopologicalSpace β] [Lattice β] [TopologicalLattice β] [AddGroup β] [IsTopologicalAddGroup β] (f : α →ₘ[μ] β) : ↑|f| =ᶠ[ae μ] fun (x : α) => |↑f x|

def MeasureTheory.AEEqFun.posPart {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] [Zero γ] (f : α →ₘ[μ] γ) : α →ₘ[μ] γ

Positive part of an AEEqFun.

@[simp]

theorem MeasureTheory.AEEqFun.posPart_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] [Zero γ] (f : α → γ) (hf : AEStronglyMeasurable f μ) : (mk f hf).posPart = mk (fun (x : α) => max (f x) 0) ⋯

theorem MeasureTheory.AEEqFun.coeFn_posPart {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] [Zero γ] (f : α →ₘ[μ] γ) : ↑f.posPart =ᶠ[ae μ] fun (a : α) => max (↑f a) 0

theorem MeasureTheory.AEEqFun.tendsto_ae_unique {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] {ι : Type u_5} [T2Space β] {g h : α → β} {f : ι → α → β} {l : Filter ι} [l.NeBot] (hg : ∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i ω) l (nhds (g ω))) (hh : ∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i ω) l (nhds (h ω))) : g =ᶠ[ae μ] h

The ae-limit is ae-unique.

def ContinuousMap.toAEEqFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [SecondCountableTopologyEither α β] [TopologicalSpace.PseudoMetrizableSpace β] (f : C(α, β)) : α →ₘ[μ] β

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

theorem ContinuousMap.coeFn_toAEEqFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [SecondCountableTopologyEither α β] [TopologicalSpace.PseudoMetrizableSpace β] (f : C(α, β)) : ↑(toAEEqFun μ f) =ᵐ[μ] ⇑f

def ContinuousMap.toAEEqFunMulHom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [SecondCountableTopologyEither α β] [TopologicalSpace.PseudoMetrizableSpace β] [Group β] [IsTopologicalGroup β] : C(α, β) →* α →ₘ[μ] β

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

def ContinuousMap.toAEEqFunAddHom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [SecondCountableTopologyEither α β] [TopologicalSpace.PseudoMetrizableSpace β] [AddGroup β] [IsTopologicalAddGroup β] : C(α, β) →+ α →ₘ[μ] β

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

def ContinuousMap.toAEEqFunLinearMap {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [TopologicalSpace α] [BorelSpace α] {𝕜 : Type u_5} [Semiring 𝕜] [TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [AddCommGroup γ] [Module 𝕜 γ] [IsTopologicalAddGroup γ] [ContinuousConstSMul 𝕜 γ] [SecondCountableTopologyEither α γ] : C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ

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