Documentation

Mathlib.MeasureTheory.Function.AEEqFun

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) [MeasurableSpace α] [TopologicalSpace β] (μ : Measure α) :

Setoid { f : α → β // AEStronglyMeasurable f μ }

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

Equations

MeasureTheory.Measure.aeEqSetoid β μ = { r := fun (f g : { f : α → β // MeasureTheory.AEStronglyMeasurable f μ }) => ↑f =ᵐ[μ] ↑g, iseqv := ⋯ }

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.

Equations

(α →ₘ[μ] β) = Quotient (MeasureTheory.Measure.aeEqSetoid β μ)

Instances For

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

MeasureTheory.AEEqFun.mk f hf = Quotient.mk'' ⟨f, hf⟩

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.

Equations

↑f = if h : ∃ (b : β), f = MeasureTheory.AEEqFun.mk (Function.const α b) ⋯ then Function.const α (Classical.choose h) else MeasureTheory.AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯

instance MeasureTheory.AEEqFun.instCoeFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace β] :

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} [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.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.

Equations

g.compQuasiMeasurePreserving f hf = Quotient.liftOn' g (fun (g : { f : β → γ // MeasureTheory.AEStronglyMeasurable f ν }) => MeasureTheory.AEEqFun.mk (↑g ∘ f) ⋯) ⋯

@[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.

Equations

g.compMeasurePreserving f hf = g.compQuasiMeasurePreserving f ⋯

@[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] : α →ₘ γ.

Equations

MeasureTheory.AEEqFun.comp g hg f = Quotient.liftOn' f (fun (f : { f : α → β // MeasureTheory.AEStronglyMeasurable f μ }) => MeasureTheory.AEEqFun.mk (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.

Equations

MeasureTheory.AEEqFun.compMeasurable g hg f = Quotient.liftOn' f (fun (f' : { f : α → β // MeasureTheory.AEStronglyMeasurable f μ }) => MeasureTheory.AEEqFun.mk (g ∘ ↑f') ⋯) ⋯

@[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).

Equations

One or more equations did not get rendered due to their size.

@[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)] : α →ₘ γ

Equations

MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.comp (Function.uncurry g) hg (f₁.pair f₂)

@[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.

Equations

MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ = MeasureTheory.AEEqFun.compMeasurable (Function.uncurry g) hg (f₁.pair f₂)

@[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.

Equations

f.toGerm = Quotient.liftOn' f (fun (f : { f : α → β // MeasureTheory.AEStronglyMeasurable f μ }) => ↑↑f) ⋯

@[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 : α →ₘ[μ] β) :

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

Equations

MeasureTheory.AEEqFun.LiftPred p f = Filter.Germ.LiftPred p f.toGerm

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

MeasureTheory.AEEqFun.LiftRel r f g = Filter.Germ.LiftRel r f.toGerm g.toGerm

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 (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instPreorder = Preorder.lift MeasureTheory.AEEqFun.toGerm

@[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 (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instPartialOrder = PartialOrder.lift MeasureTheory.AEEqFun.toGerm ⋯

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

Max (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instSup = { max := fun (f g : α →ₘ[μ] β) => MeasureTheory.AEEqFun.comp₂ (fun (x1 x2 : β) => x1 ⊔ x2) ⋯ f g }

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 (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instInf = { min := fun (f g : α →ₘ[μ] β) => MeasureTheory.AEEqFun.comp₂ (fun (x1 x2 : β) => x1 ⊓ x2) ⋯ f g }

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 (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instLattice = Lattice.mk min ⋯ ⋯ ⋯

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

Equations

MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.mk (fun (x : α) => b) ⋯

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 (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instInhabited = { default := MeasureTheory.AEEqFun.const α default }

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

One (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instOne = { one := MeasureTheory.AEEqFun.const α 1 }

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

Zero (α →ₘ[μ] β)

Equations

MeasureTheory.AEEqFun.instZero = { zero := MeasureTheory.AEEqFun.const α 0 }

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 β] :

@[simp]

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

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

SMul 𝕜 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instSMul = { smul := fun (c : 𝕜) (f : α →ₘ[μ] γ) => MeasureTheory.AEEqFun.comp (fun (x : γ) => c • x) ⋯ f }

@[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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instMul = { mul := MeasureTheory.AEEqFun.comp₂ (fun (x1 x2 : γ) => x1 * x2) ⋯ }

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

Add (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instAdd = { add := MeasureTheory.AEEqFun.comp₂ (fun (x1 x2 : γ) => x1 + x2) ⋯ }

@[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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instAddMonoid = Function.Injective.addMonoid MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯

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

AddCommMonoid (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯

instance MeasureTheory.AEEqFun.instPowNat {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] :

Pow (α →ₘ[μ] γ) ℕ

Equations

MeasureTheory.AEEqFun.instPowNat = { pow := fun (f : α →ₘ[μ] γ) (n : ℕ) => MeasureTheory.AEEqFun.comp (fun (a : γ) => a ^ n) ⋯ f }

@[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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instMonoid = Function.Injective.monoid MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯

def MeasureTheory.AEEqFun.toGermMonoidHom {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] :

(α →ₘ[μ] γ) →* (ae μ).Germ γ

AEEqFun.toGerm as a MonoidHom.

Equations

MeasureTheory.AEEqFun.toGermMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_one' := ⋯, map_mul' := ⋯ }

def MeasureTheory.AEEqFun.toGermAddMonoidHom {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] :

(α →ₘ[μ] γ) →+ (ae μ).Germ γ

AEEqFun.toGerm as an AddMonoidHom.

Equations

MeasureTheory.AEEqFun.toGermAddMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_zero' := ⋯, map_add' := ⋯ }

@[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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instCommMonoid = Function.Injective.commMonoid MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯

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

Inv (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instInv = { inv := MeasureTheory.AEEqFun.comp Inv.inv ⋯ }

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

Neg (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instNeg = { neg := MeasureTheory.AEEqFun.comp Neg.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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instDiv = { div := MeasureTheory.AEEqFun.comp₂ Div.div ⋯ }

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

Sub (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instSub = { sub := MeasureTheory.AEEqFun.comp₂ Sub.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 (α →ₘ[μ] γ) ℤ

Equations

MeasureTheory.AEEqFun.instPowInt = { pow := fun (f : α →ₘ[μ] γ) (n : ℤ) => MeasureTheory.AEEqFun.comp (fun (a : γ) => a ^ n) ⋯ f }

@[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 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instAddGroup = Function.Injective.addGroup MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

AddCommGroup (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instAddCommGroup = AddCommGroup.mk ⋯

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

Group (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instGroup = Function.Injective.group MeasureTheory.AEEqFun.toGerm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

CommGroup (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instCommGroup = CommGroup.mk ⋯

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

MulAction 𝕜 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instMulAction = Function.Injective.mulAction MeasureTheory.AEEqFun.toGerm ⋯ ⋯

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

DistribMulAction 𝕜 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instDistribMulAction = Function.Injective.distribMulAction MeasureTheory.AEEqFun.toGermAddMonoidHom ⋯ ⋯

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

Module 𝕜 (α →ₘ[μ] γ)

Equations

MeasureTheory.AEEqFun.instModule = Function.Injective.module 𝕜 MeasureTheory.AEEqFun.toGermAddMonoidHom ⋯ ⋯

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

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

Equations

f.lintegral = Quotient.liftOn' f (fun (f : { f : α → ENNReal // MeasureTheory.AEStronglyMeasurable f μ }) => ∫⁻ (a : α), ↑f a ∂μ) ⋯

@[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.

Equations

f.posPart = MeasureTheory.AEEqFun.comp (fun (x : γ) => x ⊔ 0) ⋯ f

@[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 : α) => 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 : α) => ↑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.

Equations

ContinuousMap.toAEEqFun μ f = MeasureTheory.AEEqFun.mk ⇑f ⋯

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.

Equations

ContinuousMap.toAEEqFunMulHom μ = { toFun := ContinuousMap.toAEEqFun μ, map_one' := ⋯, map_mul' := ⋯ }

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.

Equations

ContinuousMap.toAEEqFunAddHom μ = { toFun := ContinuousMap.toAEEqFun μ, map_zero' := ⋯, map_add' := ⋯ }

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.

Equations

ContinuousMap.toAEEqFunLinearMap μ = { toFun := (↑(ContinuousMap.toAEEqFunAddHom μ)).toFun, map_add' := ⋯, map_smul' := ⋯ }