Almost everywhere equal functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We build a space of equivalence classes of functions, where two functions are treated as identical
if they are almost everywhere equal. We form the set of equivalence classes under the relation of
being almost everywhere equal, which is sometimes known as the L⁰ space.
To use this space as a basis for the L^p spaces and for the Bochner integral, we consider
equivalence classes of strongly measurable functions (or, equivalently, of almost everywhere
strongly measurable functions.)
See l1_space.lean for L¹ space.
Notation #
-
α →ₘ[μ] βis the type ofL⁰space, whereαis a measurable space,βis a topological space, andμis a measure onα.f : α →ₘ βis a "function" inL⁰. In comments,[f]is also used to denote anL⁰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 onL⁰in the natural way, i.e.,[f] + [g] := [f + g],c • [f] := [c • f]. So defined,α →ₘ βinherits the linear structure ofβ. For example, ifβis a module, thenα →ₘ βis a module over the same ring.See
mk_add_mk,neg_mk,mk_sub_mk,smul_mk,add_to_fun,neg_to_fun,sub_to_fun,smul_to_fun -
The order structure of
L⁰:≤can be defined in a similar way:[f] ≤ [g]iff a ≤ g afor almost allain domain. Andα →ₘ βinherits the preorder and partial order ofβ.TODO: Define
supandinfonL⁰so that it forms a lattice. It seems thatβmust be a linear order, since otherwisef ⊔ gmay not be a measurable function.
Implementation notes #
f.to_fun: To find a representative off : α →ₘ β, use the coercion(f : α → β), which is implemented asf.to_fun. For each operationopinL⁰, there is a lemma calledcoe_fn_op, characterizing, say,(f op g : α → β).ae_eq_fun.mk: To constructs anL⁰functionα →ₘ βfrom an almost everywhere strongly measurable functionf : α → β, useae_eq_fun.mkcomp: Usecomp g fto get[g ∘ f]fromg : β → γand[f] : α →ₘ γwhengis continuous. Usecomp_measurableifgis only measurable (this requires the target space to be second countable).comp₂: Usecomp₂ g f₁ f₂ to get[λ a, g (f₁ a) (f₂ a)]. For example,[f + g]iscomp₂ (+)`
Tags #
function space, almost everywhere equal, L⁰, ae_eq_fun
def
measure_theory.measure.ae_eq_setoid
{α : Type u_1}
(β : Type u_2)
[measurable_space α]
[topological_space β]
(μ : measure_theory.measure α) :
setoid {f // measure_theory.ae_strongly_measurable f μ}
The equivalence relation of being almost everywhere equal for almost everywhere strongly measurable functions.
Equations
- measure_theory.measure.ae_eq_setoid β μ = {r := λ (f g : {f // measure_theory.ae_strongly_measurable f μ}), ↑f =ᵐ[μ] ↑g, iseqv := _}
def
measure_theory.ae_eq_fun
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[topological_space β]
(μ : measure_theory.measure α) :
Type (max u_1 u_2)
The space of equivalence classes of almost everywhere strongly measurable functions, where two
strongly measurable functions are equivalent if they agree almost everywhere, i.e.,
they differ on a set of measure 0.
Equations
- (α →ₘ[μ] β) = quotient (measure_theory.measure.ae_eq_setoid β μ)
Instances for measure_theory.ae_eq_fun
- measure_theory.ae_eq_fun.has_coe_to_fun
- measure_theory.ae_eq_fun.preorder
- measure_theory.ae_eq_fun.partial_order
- measure_theory.ae_eq_fun.has_sup
- measure_theory.ae_eq_fun.has_inf
- measure_theory.ae_eq_fun.lattice
- measure_theory.ae_eq_fun.inhabited
- measure_theory.ae_eq_fun.has_one
- measure_theory.ae_eq_fun.has_zero
- measure_theory.ae_eq_fun.has_smul
- measure_theory.ae_eq_fun.smul_comm_class
- measure_theory.ae_eq_fun.is_scalar_tower
- measure_theory.ae_eq_fun.is_central_scalar
- measure_theory.ae_eq_fun.has_mul
- measure_theory.ae_eq_fun.has_add
- measure_theory.ae_eq_fun.add_monoid
- measure_theory.ae_eq_fun.add_comm_monoid
- measure_theory.ae_eq_fun.nat.has_pow
- measure_theory.ae_eq_fun.monoid
- measure_theory.ae_eq_fun.comm_monoid
- measure_theory.ae_eq_fun.has_inv
- measure_theory.ae_eq_fun.has_neg
- measure_theory.ae_eq_fun.has_div
- measure_theory.ae_eq_fun.has_sub
- measure_theory.ae_eq_fun.has_int_pow
- measure_theory.ae_eq_fun.add_group
- measure_theory.ae_eq_fun.add_comm_group
- measure_theory.ae_eq_fun.group
- measure_theory.ae_eq_fun.comm_group
- measure_theory.ae_eq_fun.mul_action
- measure_theory.ae_eq_fun.distrib_mul_action
- measure_theory.ae_eq_fun.module
def
measure_theory.ae_eq_fun.mk
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[topological_space β]
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
Construct the equivalence class [f] of an almost everywhere measurable function f, based
on the equivalence relation of being almost everywhere equal.
Equations
- measure_theory.ae_eq_fun.mk f hf = quotient.mk' ⟨f, hf⟩
@[protected, instance]
noncomputable
def
measure_theory.ae_eq_fun.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β] :
A measurable representative of an ae_eq_fun [f]
Equations
- measure_theory.ae_eq_fun.has_coe_to_fun = {coe := λ (f : α →ₘ[μ] β), measure_theory.ae_strongly_measurable.mk (quotient.out' f).val _}
@[protected]
theorem
measure_theory.ae_eq_fun.strongly_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
(f : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.ae_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
(f : α →ₘ[μ] β) :
ae_measurable ⇑f μ
@[simp]
theorem
measure_theory.ae_eq_fun.quot_mk_eq_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
quot.mk setoid.r ⟨f, hf⟩ = measure_theory.ae_eq_fun.mk f hf
@[simp]
theorem
measure_theory.ae_eq_fun.mk_eq_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
{hf : measure_theory.ae_strongly_measurable f μ}
{hg : measure_theory.ae_strongly_measurable g μ} :
measure_theory.ae_eq_fun.mk f hf = measure_theory.ae_eq_fun.mk g hg ↔ f =ᵐ[μ] g
@[simp]
theorem
measure_theory.ae_eq_fun.mk_coe_fn
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β) :
@[ext]
theorem
measure_theory.ae_eq_fun.ext
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
{f g : α →ₘ[μ] β}
(h : ⇑f =ᵐ[μ] ⇑g) :
f = g
theorem
measure_theory.ae_eq_fun.ext_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
{f g : α →ₘ[μ] β} :
theorem
measure_theory.ae_eq_fun.coe_fn_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
⇑(measure_theory.ae_eq_fun.mk f hf) =ᵐ[μ] f
theorem
measure_theory.ae_eq_fun.induction_on
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β)
{p : (α →ₘ[μ] β) → Prop}
(H : ∀ (f : α → β) (hf : measure_theory.ae_strongly_measurable f μ), p (measure_theory.ae_eq_fun.mk f hf)) :
p f
theorem
measure_theory.ae_eq_fun.induction_on₂
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
{α' : Type u_3}
{β' : Type u_4}
[measurable_space α']
[topological_space β']
{μ' : measure_theory.measure α'}
(f : α →ₘ[μ] β)
(f' : α' →ₘ[μ'] β')
{p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop}
(H : ∀ (f : α → β) (hf : measure_theory.ae_strongly_measurable f μ) (f' : α' → β') (hf' : measure_theory.ae_strongly_measurable f' μ'), p (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk f' hf')) :
p f f'
theorem
measure_theory.ae_eq_fun.induction_on₃
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
{α' : Type u_3}
{β' : Type u_4}
[measurable_space α']
[topological_space β']
{μ' : measure_theory.measure α'}
{α'' : Type u_5}
{β'' : Type u_6}
[measurable_space α'']
[topological_space β'']
{μ'' : measure_theory.measure α''}
(f : α →ₘ[μ] β)
(f' : α' →ₘ[μ'] β')
(f'' : α'' →ₘ[μ''] β'')
{p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop}
(H : ∀ (f : α → β) (hf : measure_theory.ae_strongly_measurable f μ) (f' : α' → β') (hf' : measure_theory.ae_strongly_measurable f' μ') (f'' : α'' → β'') (hf'' : measure_theory.ae_strongly_measurable f'' μ''), p (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk f' hf') (measure_theory.ae_eq_fun.mk f'' hf'')) :
p f f' f''
def
measure_theory.ae_eq_fun.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(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
- measure_theory.ae_eq_fun.comp g hg f = quotient.lift_on' f (λ (f : {f // measure_theory.ae_strongly_measurable f μ}), measure_theory.ae_eq_fun.mk (g ∘ ↑f) _) _
@[simp]
theorem
measure_theory.ae_eq_fun.comp_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(g : β → γ)
(hg : continuous g)
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_eq_fun.comp g hg (measure_theory.ae_eq_fun.mk f hf) = measure_theory.ae_eq_fun.mk (g ∘ f) _
theorem
measure_theory.ae_eq_fun.comp_eq_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(g : β → γ)
(hg : continuous g)
(f : α →ₘ[μ] β) :
measure_theory.ae_eq_fun.comp g hg f = measure_theory.ae_eq_fun.mk (g ∘ ⇑f) _
theorem
measure_theory.ae_eq_fun.coe_fn_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(g : β → γ)
(hg : continuous g)
(f : α →ₘ[μ] β) :
def
measure_theory.ae_eq_fun.comp_measurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[opens_measurable_space γ]
[topological_space.second_countable_topology γ]
(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
- measure_theory.ae_eq_fun.comp_measurable g hg f = quotient.lift_on' f (λ (f' : {f // measure_theory.ae_strongly_measurable f μ}), measure_theory.ae_eq_fun.mk (g ∘ ↑f') _) _
@[simp]
theorem
measure_theory.ae_eq_fun.comp_measurable_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[opens_measurable_space γ]
[topological_space.second_countable_topology γ]
(g : β → γ)
(hg : measurable g)
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_eq_fun.comp_measurable g hg (measure_theory.ae_eq_fun.mk f hf) = measure_theory.ae_eq_fun.mk (g ∘ f) _
theorem
measure_theory.ae_eq_fun.comp_measurable_eq_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[opens_measurable_space γ]
[topological_space.second_countable_topology γ]
(g : β → γ)
(hg : measurable g)
(f : α →ₘ[μ] β) :
measure_theory.ae_eq_fun.comp_measurable g hg f = measure_theory.ae_eq_fun.mk (g ∘ ⇑f) _
theorem
measure_theory.ae_eq_fun.coe_fn_comp_measurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[opens_measurable_space γ]
[topological_space.second_countable_topology γ]
(g : β → γ)
(hg : measurable g)
(f : α →ₘ[μ] β) :
def
measure_theory.ae_eq_fun.pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(f : α →ₘ[μ] β)
(g : α →ₘ[μ] γ) :
The class of x ↦ (f x, g x).
Equations
- f.pair g = quotient.lift_on₂' f g (λ (f : {f // measure_theory.ae_strongly_measurable f μ}) (g : {f // measure_theory.ae_strongly_measurable f μ}), measure_theory.ae_eq_fun.mk (λ (x : α), (f.val x, g.val x)) _) measure_theory.ae_eq_fun.pair._proof_2
@[simp]
theorem
measure_theory.ae_eq_fun.pair_mk_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ)
(g : α → γ)
(hg : measure_theory.ae_strongly_measurable g μ) :
(measure_theory.ae_eq_fun.mk f hf).pair (measure_theory.ae_eq_fun.mk g hg) = measure_theory.ae_eq_fun.mk (λ (x : α), (f x, g x)) _
theorem
measure_theory.ae_eq_fun.pair_eq_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(f : α →ₘ[μ] β)
(g : α →ₘ[μ] γ) :
f.pair g = measure_theory.ae_eq_fun.mk (λ (x : α), (⇑f x, ⇑g x)) _
theorem
measure_theory.ae_eq_fun.coe_fn_pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(f : α →ₘ[μ] β)
(g : α →ₘ[μ] γ) :
def
measure_theory.ae_eq_fun.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(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
λ a, g (f₁ a) (f₂ a), i.e., the almost everywhere equal function
[λ a, g (f₁ a) (f₂ a)] : α →ₘ γ
Equations
- measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.comp (function.uncurry g) hg (f₁.pair f₂)
@[simp]
theorem
measure_theory.ae_eq_fun.comp₂_mk_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(g : β → γ → δ)
(hg : continuous (function.uncurry g))
(f₁ : α → β)
(f₂ : α → γ)
(hf₁ : measure_theory.ae_strongly_measurable f₁ μ)
(hf₂ : measure_theory.ae_strongly_measurable f₂ μ) :
measure_theory.ae_eq_fun.comp₂ g hg (measure_theory.ae_eq_fun.mk f₁ hf₁) (measure_theory.ae_eq_fun.mk f₂ hf₂) = measure_theory.ae_eq_fun.mk (λ (a : α), g (f₁ a) (f₂ a)) _
theorem
measure_theory.ae_eq_fun.comp₂_eq_pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(g : β → γ → δ)
(hg : continuous (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.comp (function.uncurry g) hg (f₁.pair f₂)
theorem
measure_theory.ae_eq_fun.comp₂_eq_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(g : β → γ → δ)
(hg : continuous (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂ = measure_theory.ae_eq_fun.mk (λ (a : α), g (⇑f₁ a) (⇑f₂ a)) _
theorem
measure_theory.ae_eq_fun.coe_fn_comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(g : β → γ → δ)
(hg : continuous (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
def
measure_theory.ae_eq_fun.comp₂_measurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[measurable_space δ]
[topological_space.pseudo_metrizable_space δ]
[opens_measurable_space δ]
[topological_space.second_countable_topology δ]
(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
λ a, g (f₁ a) (f₂ a), i.e., the almost everywhere equal function
[λ a, g (f₁ a) (f₂ a)] : α →ₘ γ. This requires δ to have second-countable topology.
Equations
- measure_theory.ae_eq_fun.comp₂_measurable g hg f₁ f₂ = measure_theory.ae_eq_fun.comp_measurable (function.uncurry g) hg (f₁.pair f₂)
@[simp]
theorem
measure_theory.ae_eq_fun.comp₂_measurable_mk_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[measurable_space δ]
[topological_space.pseudo_metrizable_space δ]
[opens_measurable_space δ]
[topological_space.second_countable_topology δ]
(g : β → γ → δ)
(hg : measurable (function.uncurry g))
(f₁ : α → β)
(f₂ : α → γ)
(hf₁ : measure_theory.ae_strongly_measurable f₁ μ)
(hf₂ : measure_theory.ae_strongly_measurable f₂ μ) :
measure_theory.ae_eq_fun.comp₂_measurable g hg (measure_theory.ae_eq_fun.mk f₁ hf₁) (measure_theory.ae_eq_fun.mk f₂ hf₂) = measure_theory.ae_eq_fun.mk (λ (a : α), g (f₁ a) (f₂ a)) _
theorem
measure_theory.ae_eq_fun.comp₂_measurable_eq_pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[measurable_space δ]
[topological_space.pseudo_metrizable_space δ]
[opens_measurable_space δ]
[topological_space.second_countable_topology δ]
(g : β → γ → δ)
(hg : measurable (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂_measurable g hg f₁ f₂ = measure_theory.ae_eq_fun.comp_measurable (function.uncurry g) hg (f₁.pair f₂)
theorem
measure_theory.ae_eq_fun.comp₂_measurable_eq_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[measurable_space δ]
[topological_space.pseudo_metrizable_space δ]
[opens_measurable_space δ]
[topological_space.second_countable_topology δ]
(g : β → γ → δ)
(hg : measurable (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
measure_theory.ae_eq_fun.comp₂_measurable g hg f₁ f₂ = measure_theory.ae_eq_fun.mk (λ (a : α), g (⇑f₁ a) (⇑f₂ a)) _
theorem
measure_theory.ae_eq_fun.coe_fn_comp₂_measurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
[measurable_space γ]
[topological_space.pseudo_metrizable_space γ]
[borel_space γ]
[topological_space.second_countable_topology γ]
[measurable_space δ]
[topological_space.pseudo_metrizable_space δ]
[opens_measurable_space δ]
[topological_space.second_countable_topology δ]
(g : β → γ → δ)
(hg : measurable (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
def
measure_theory.ae_eq_fun.to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β) :
Interpret f : α →ₘ[μ] β as a germ at μ.ae forgetting that f is almost everywhere
strongly measurable.
Equations
- f.to_germ = quotient.lift_on' f (λ (f : {f // measure_theory.ae_strongly_measurable f μ}), ↑↑f) measure_theory.ae_eq_fun.to_germ._proof_1
@[simp]
theorem
measure_theory.ae_eq_fun.mk_to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α → β)
(hf : measure_theory.ae_strongly_measurable f μ) :
(measure_theory.ae_eq_fun.mk f hf).to_germ = ↑f
theorem
measure_theory.ae_eq_fun.to_germ_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(f : α →ₘ[μ] β) :
theorem
measure_theory.ae_eq_fun.to_germ_injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β] :
theorem
measure_theory.ae_eq_fun.comp_to_germ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(g : β → γ)
(hg : continuous g)
(f : α →ₘ[μ] β) :
(measure_theory.ae_eq_fun.comp g hg f).to_germ = filter.germ.map g f.to_germ
theorem
measure_theory.ae_eq_fun.comp_measurable_to_germ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[measurable_space β]
[borel_space β]
[topological_space.pseudo_metrizable_space β]
[topological_space.pseudo_metrizable_space γ]
[topological_space.second_countable_topology γ]
[measurable_space γ]
[opens_measurable_space γ]
(g : β → γ)
(hg : measurable g)
(f : α →ₘ[μ] β) :
theorem
measure_theory.ae_eq_fun.comp₂_to_germ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
(g : β → γ → δ)
(hg : continuous (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
(measure_theory.ae_eq_fun.comp₂ g hg f₁ f₂).to_germ = filter.germ.map₂ g f₁.to_germ f₂.to_germ
theorem
measure_theory.ae_eq_fun.comp₂_measurable_to_germ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
[topological_space δ]
[topological_space.pseudo_metrizable_space β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
[topological_space.pseudo_metrizable_space γ]
[topological_space.second_countable_topology γ]
[measurable_space γ]
[borel_space γ]
[topological_space.pseudo_metrizable_space δ]
[topological_space.second_countable_topology δ]
[measurable_space δ]
[opens_measurable_space δ]
(g : β → γ → δ)
(hg : measurable (function.uncurry g))
(f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ) :
(measure_theory.ae_eq_fun.comp₂_measurable g hg f₁ f₂).to_germ = filter.germ.map₂ g f₁.to_germ f₂.to_germ
def
measure_theory.ae_eq_fun.lift_pred
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(p : β → Prop)
(f : α →ₘ[μ] β) :
Prop
Given a predicate p and an equivalence class [f], return true if p holds of f a
for almost all a
Equations
def
measure_theory.ae_eq_fun.lift_rel
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
(r : β → γ → Prop)
(f : α →ₘ[μ] β)
(g : α →ₘ[μ] γ) :
Prop
Given a relation r and equivalence class [f] and [g], return true if r holds of
(f a, g a) for almost all a
Equations
theorem
measure_theory.ae_eq_fun.lift_rel_mk_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{hf : measure_theory.ae_strongly_measurable f μ}
{hg : measure_theory.ae_strongly_measurable g μ} :
measure_theory.ae_eq_fun.lift_rel r (measure_theory.ae_eq_fun.mk f hf) (measure_theory.ae_eq_fun.mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (f a) (g a)
theorem
measure_theory.ae_eq_fun.lift_rel_iff_coe_fn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[topological_space γ]
{r : β → γ → Prop}
{f : α →ₘ[μ] β}
{g : α →ₘ[μ] γ} :
@[protected, instance]
def
measure_theory.ae_eq_fun.preorder
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[preorder β] :
@[simp]
theorem
measure_theory.ae_eq_fun.mk_le_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[preorder β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_eq_fun.mk f hf ≤ measure_theory.ae_eq_fun.mk g hg ↔ f ≤ᵐ[μ] g
@[simp, norm_cast]
theorem
measure_theory.ae_eq_fun.coe_fn_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[preorder β]
{f g : α →ₘ[μ] β} :
@[protected, instance]
def
measure_theory.ae_eq_fun.partial_order
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[partial_order β] :
partial_order (α →ₘ[μ] β)
@[protected, instance]
def
measure_theory.ae_eq_fun.has_sup
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_sup β]
[has_continuous_sup β] :
Equations
- measure_theory.ae_eq_fun.has_sup = {sup := λ (f g : α →ₘ[μ] β), measure_theory.ae_eq_fun.comp₂ has_sup.sup measure_theory.ae_eq_fun.has_sup._proof_1 f g}
theorem
measure_theory.ae_eq_fun.coe_fn_sup
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_sup β]
[has_continuous_sup β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.le_sup_left
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_sup β]
[has_continuous_sup β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.le_sup_right
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_sup β]
[has_continuous_sup β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.sup_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_sup β]
[has_continuous_sup β]
(f g f' : α →ₘ[μ] β)
(hf : f ≤ f')
(hg : g ≤ f') :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_inf
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_inf β]
[has_continuous_inf β] :
Equations
- measure_theory.ae_eq_fun.has_inf = {inf := λ (f g : α →ₘ[μ] β), measure_theory.ae_eq_fun.comp₂ has_inf.inf measure_theory.ae_eq_fun.has_inf._proof_1 f g}
theorem
measure_theory.ae_eq_fun.coe_fn_inf
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_inf β]
[has_continuous_inf β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.inf_le_left
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_inf β]
[has_continuous_inf β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.inf_le_right
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_inf β]
[has_continuous_inf β]
(f g : α →ₘ[μ] β) :
@[protected]
theorem
measure_theory.ae_eq_fun.le_inf
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[semilattice_inf β]
[has_continuous_inf β]
(f' f g : α →ₘ[μ] β)
(hf : f' ≤ f)
(hg : f' ≤ g) :
@[protected, instance]
def
measure_theory.ae_eq_fun.lattice
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[lattice β]
[topological_lattice β] :
Equations
- measure_theory.ae_eq_fun.lattice = {sup := has_sup.sup measure_theory.ae_eq_fun.has_sup, le := partial_order.le measure_theory.ae_eq_fun.partial_order, lt := partial_order.lt measure_theory.ae_eq_fun.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf measure_theory.ae_eq_fun.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
measure_theory.ae_eq_fun.const
(α : Type u_1)
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(b : β) :
The equivalence class of a constant function: [λ a:α, b], based on the equivalence relation of
being almost everywhere equal
Equations
theorem
measure_theory.ae_eq_fun.coe_fn_const
(α : Type u_1)
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
(b : β) :
⇑(measure_theory.ae_eq_fun.const α b) =ᵐ[μ] function.const α b
@[protected, instance]
def
measure_theory.ae_eq_fun.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[inhabited β] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_zero β] :
Equations
@[protected, instance]
def
measure_theory.ae_eq_fun.has_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_one β] :
Equations
theorem
measure_theory.ae_eq_fun.one_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_one β] :
1 = measure_theory.ae_eq_fun.mk (λ (a : α), 1) measure_theory.ae_strongly_measurable_const
theorem
measure_theory.ae_eq_fun.zero_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_zero β] :
0 = measure_theory.ae_eq_fun.mk (λ (a : α), 0) measure_theory.ae_strongly_measurable_const
theorem
measure_theory.ae_eq_fun.coe_fn_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_zero β] :
theorem
measure_theory.ae_eq_fun.coe_fn_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_one β] :
@[simp]
theorem
measure_theory.ae_eq_fun.zero_to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_zero β] :
@[simp]
theorem
measure_theory.ae_eq_fun.one_to_germ
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space β]
[has_one β] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_smul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ] :
Equations
- measure_theory.ae_eq_fun.has_smul = {smul := λ (c : 𝕜) (f : α →ₘ[μ] γ), measure_theory.ae_eq_fun.comp (has_smul.smul c) _ f}
@[simp]
theorem
measure_theory.ae_eq_fun.smul_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
(c : 𝕜)
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ) :
c • measure_theory.ae_eq_fun.mk f hf = measure_theory.ae_eq_fun.mk (c • f) _
theorem
measure_theory.ae_eq_fun.coe_fn_smul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
(c : 𝕜)
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.smul_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
(c : 𝕜)
(f : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.smul_comm_class
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
{𝕜' : Type u_6}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
[has_smul 𝕜' γ]
[has_continuous_const_smul 𝕜' γ]
[smul_comm_class 𝕜 𝕜' γ] :
smul_comm_class 𝕜 𝕜' (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.is_scalar_tower
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
{𝕜' : Type u_6}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
[has_smul 𝕜' γ]
[has_continuous_const_smul 𝕜' γ]
[has_smul 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' γ] :
is_scalar_tower 𝕜 𝕜' (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.is_central_scalar
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[has_smul 𝕜 γ]
[has_continuous_const_smul 𝕜 γ]
[has_smul 𝕜ᵐᵒᵖ γ]
[is_central_scalar 𝕜 γ] :
is_central_scalar 𝕜 (α →ₘ[μ] γ)
@[protected, instance]
def
measure_theory.ae_eq_fun.has_add
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_add γ]
[has_continuous_add γ] :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_mul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_mul γ]
[has_continuous_mul γ] :
@[simp]
theorem
measure_theory.ae_eq_fun.mk_mul_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_mul γ]
[has_continuous_mul γ]
(f g : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_eq_fun.mk f hf * measure_theory.ae_eq_fun.mk g hg = measure_theory.ae_eq_fun.mk (f * g) _
@[simp]
theorem
measure_theory.ae_eq_fun.mk_add_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_add γ]
[has_continuous_add γ]
(f g : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_eq_fun.mk f hf + measure_theory.ae_eq_fun.mk g hg = measure_theory.ae_eq_fun.mk (f + g) _
theorem
measure_theory.ae_eq_fun.coe_fn_mul
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_mul γ]
[has_continuous_mul γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_add
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_add γ]
[has_continuous_add γ]
(f g : α →ₘ[μ] γ) :
@[simp]
theorem
measure_theory.ae_eq_fun.mul_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_mul γ]
[has_continuous_mul γ]
(f g : α →ₘ[μ] γ) :
@[simp]
theorem
measure_theory.ae_eq_fun.add_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[has_add γ]
[has_continuous_add γ]
(f g : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.add_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_monoid γ]
[has_continuous_add γ] :
add_monoid (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.add_monoid = function.injective.add_monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.add_monoid._proof_1 measure_theory.ae_eq_fun.add_monoid._proof_2 measure_theory.ae_eq_fun.add_monoid._proof_3
@[protected, instance]
def
measure_theory.ae_eq_fun.add_comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_comm_monoid γ]
[has_continuous_add γ] :
add_comm_monoid (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.add_comm_monoid = function.injective.add_comm_monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.add_comm_monoid._proof_2 measure_theory.ae_eq_fun.add_comm_monoid._proof_3 measure_theory.ae_eq_fun.add_comm_monoid._proof_4
@[protected, instance]
def
measure_theory.ae_eq_fun.nat.has_pow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ] :
Equations
- measure_theory.ae_eq_fun.nat.has_pow = {pow := λ (f : α →ₘ[μ] γ) (n : ℕ), measure_theory.ae_eq_fun.comp (λ (a : γ), a ^ n) _ f}
@[simp]
theorem
measure_theory.ae_eq_fun.mk_pow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ]
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(n : ℕ) :
measure_theory.ae_eq_fun.mk f hf ^ n = measure_theory.ae_eq_fun.mk (f ^ n) _
theorem
measure_theory.ae_eq_fun.coe_fn_pow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ]
(f : α →ₘ[μ] γ)
(n : ℕ) :
@[simp]
theorem
measure_theory.ae_eq_fun.pow_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ]
(f : α →ₘ[μ] γ)
(n : ℕ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ] :
Equations
- measure_theory.ae_eq_fun.monoid = function.injective.monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.monoid._proof_1 measure_theory.ae_eq_fun.monoid._proof_2 measure_theory.ae_eq_fun.pow_to_germ
def
measure_theory.ae_eq_fun.to_germ_monoid_hom
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ] :
ae_eq_fun.to_germ as a monoid_hom.
Equations
- measure_theory.ae_eq_fun.to_germ_monoid_hom = {to_fun := measure_theory.ae_eq_fun.to_germ _inst_3, map_one' := _, map_mul' := _}
def
measure_theory.ae_eq_fun.to_germ_add_monoid_hom
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_monoid γ]
[has_continuous_add γ] :
ae_eq_fun.to_germ as an add_monoid_hom.
Equations
- measure_theory.ae_eq_fun.to_germ_add_monoid_hom = {to_fun := measure_theory.ae_eq_fun.to_germ _inst_3, map_zero' := _, map_add' := _}
@[simp]
theorem
measure_theory.ae_eq_fun.to_germ_monoid_hom_apply
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[monoid γ]
[has_continuous_mul γ]
(f : α →ₘ[μ] γ) :
@[simp]
theorem
measure_theory.ae_eq_fun.to_germ_add_monoid_hom_apply
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_monoid γ]
[has_continuous_add γ]
(f : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.comm_monoid
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[comm_monoid γ]
[has_continuous_mul γ] :
comm_monoid (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.comm_monoid = function.injective.comm_monoid measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.comm_monoid._proof_1 measure_theory.ae_eq_fun.comm_monoid._proof_2 measure_theory.ae_eq_fun.comm_monoid._proof_3
@[protected, instance]
def
measure_theory.ae_eq_fun.has_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ] :
Equations
- measure_theory.ae_eq_fun.has_neg = {neg := measure_theory.ae_eq_fun.comp has_neg.neg measure_theory.ae_eq_fun.has_neg._proof_1}
@[protected, instance]
def
measure_theory.ae_eq_fun.has_inv
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ] :
Equations
- measure_theory.ae_eq_fun.has_inv = {inv := measure_theory.ae_eq_fun.comp has_inv.inv measure_theory.ae_eq_fun.has_inv._proof_1}
@[simp]
theorem
measure_theory.ae_eq_fun.neg_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ) :
@[simp]
theorem
measure_theory.ae_eq_fun.inv_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ) :
theorem
measure_theory.ae_eq_fun.coe_fn_inv
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_neg
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.neg_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.inv_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_sub
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ] :
Equations
- measure_theory.ae_eq_fun.has_sub = {sub := measure_theory.ae_eq_fun.comp₂ has_sub.sub measure_theory.ae_eq_fun.has_sub._proof_1}
@[protected, instance]
def
measure_theory.ae_eq_fun.has_div
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ] :
Equations
- measure_theory.ae_eq_fun.has_div = {div := measure_theory.ae_eq_fun.comp₂ has_div.div measure_theory.ae_eq_fun.has_div._proof_1}
@[simp]
theorem
measure_theory.ae_eq_fun.mk_div
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f g : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_eq_fun.mk (f / g) _ = measure_theory.ae_eq_fun.mk f hf / measure_theory.ae_eq_fun.mk g hg
@[simp]
theorem
measure_theory.ae_eq_fun.mk_sub
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f g : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_eq_fun.mk (f - g) _ = measure_theory.ae_eq_fun.mk f hf - measure_theory.ae_eq_fun.mk g hg
theorem
measure_theory.ae_eq_fun.coe_fn_sub
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.coe_fn_div
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.sub_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ]
(f g : α →ₘ[μ] γ) :
theorem
measure_theory.ae_eq_fun.div_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f g : α →ₘ[μ] γ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.has_int_pow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ] :
Equations
- measure_theory.ae_eq_fun.has_int_pow = {pow := λ (f : α →ₘ[μ] γ) (n : ℤ), measure_theory.ae_eq_fun.comp (λ (a : γ), a ^ n) _ f}
@[simp]
theorem
measure_theory.ae_eq_fun.mk_zpow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ)
(n : ℤ) :
measure_theory.ae_eq_fun.mk f hf ^ n = measure_theory.ae_eq_fun.mk (f ^ n) _
theorem
measure_theory.ae_eq_fun.coe_fn_zpow
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ)
(n : ℤ) :
@[simp]
theorem
measure_theory.ae_eq_fun.zpow_to_germ
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ]
(f : α →ₘ[μ] γ)
(n : ℤ) :
@[protected, instance]
def
measure_theory.ae_eq_fun.add_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_group γ]
[topological_add_group γ] :
Equations
- measure_theory.ae_eq_fun.add_group = function.injective.add_group measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.add_group._proof_2 measure_theory.ae_eq_fun.add_group._proof_3 measure_theory.ae_eq_fun.neg_to_germ measure_theory.ae_eq_fun.sub_to_germ measure_theory.ae_eq_fun.add_group._proof_4 measure_theory.ae_eq_fun.add_group._proof_5
@[protected, instance]
def
measure_theory.ae_eq_fun.add_comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[add_comm_group γ]
[topological_add_group γ] :
add_comm_group (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.add_comm_group = function.injective.add_comm_group measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.add_comm_group._proof_4 measure_theory.ae_eq_fun.add_comm_group._proof_5 measure_theory.ae_eq_fun.add_comm_group._proof_6 measure_theory.ae_eq_fun.add_comm_group._proof_7 measure_theory.ae_eq_fun.add_comm_group._proof_8 measure_theory.ae_eq_fun.add_comm_group._proof_9
@[protected, instance]
def
measure_theory.ae_eq_fun.group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[group γ]
[topological_group γ] :
Equations
- measure_theory.ae_eq_fun.group = function.injective.group measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.group._proof_1 measure_theory.ae_eq_fun.group._proof_2 measure_theory.ae_eq_fun.inv_to_germ measure_theory.ae_eq_fun.div_to_germ measure_theory.ae_eq_fun.group._proof_3 measure_theory.ae_eq_fun.zpow_to_germ
@[protected, instance]
def
measure_theory.ae_eq_fun.comm_group
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[comm_group γ]
[topological_group γ] :
comm_group (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.comm_group = function.injective.comm_group measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.comm_group._proof_3 measure_theory.ae_eq_fun.comm_group._proof_4 measure_theory.ae_eq_fun.comm_group._proof_5 measure_theory.ae_eq_fun.comm_group._proof_6 measure_theory.ae_eq_fun.comm_group._proof_7 measure_theory.ae_eq_fun.comm_group._proof_8
@[protected, instance]
def
measure_theory.ae_eq_fun.mul_action
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[monoid 𝕜]
[mul_action 𝕜 γ]
[has_continuous_const_smul 𝕜 γ] :
mul_action 𝕜 (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.mul_action = function.injective.mul_action measure_theory.ae_eq_fun.to_germ measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.mul_action._proof_1
@[protected, instance]
def
measure_theory.ae_eq_fun.distrib_mul_action
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[monoid 𝕜]
[add_monoid γ]
[has_continuous_add γ]
[distrib_mul_action 𝕜 γ]
[has_continuous_const_smul 𝕜 γ] :
distrib_mul_action 𝕜 (α →ₘ[μ] γ)
Equations
- measure_theory.ae_eq_fun.distrib_mul_action = function.injective.distrib_mul_action measure_theory.ae_eq_fun.to_germ_add_monoid_hom measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.distrib_mul_action._proof_1
@[protected, instance]
def
measure_theory.ae_eq_fun.module
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
{𝕜 : Type u_5}
[semiring 𝕜]
[add_comm_monoid γ]
[has_continuous_add γ]
[module 𝕜 γ]
[has_continuous_const_smul 𝕜 γ] :
Equations
- measure_theory.ae_eq_fun.module = function.injective.module 𝕜 measure_theory.ae_eq_fun.to_germ_add_monoid_hom measure_theory.ae_eq_fun.to_germ_injective measure_theory.ae_eq_fun.module._proof_1
noncomputable
def
measure_theory.ae_eq_fun.lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →ₘ[μ] ennreal) :
For f : α → ℝ≥0∞, define ∫ [f] to be ∫ f
Equations
- f.lintegral = quotient.lift_on' f (λ (f : {f // measure_theory.ae_strongly_measurable f μ}), ∫⁻ (a : α), ↑f a ∂μ) measure_theory.ae_eq_fun.lintegral._proof_1
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_mk
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → ennreal)
(hf : measure_theory.ae_strongly_measurable f μ) :
theorem
measure_theory.ae_eq_fun.lintegral_coe_fn
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →ₘ[μ] ennreal) :
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.ae_eq_fun.lintegral_eq_zero_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α →ₘ[μ] ennreal} :
theorem
measure_theory.ae_eq_fun.lintegral_add
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f g : α →ₘ[μ] ennreal) :
theorem
measure_theory.ae_eq_fun.lintegral_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α →ₘ[μ] ennreal} :
theorem
measure_theory.ae_eq_fun.coe_fn_abs
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[topological_space β]
[lattice β]
[topological_lattice β]
[add_group β]
[topological_add_group β]
(f : α →ₘ[μ] β) :
def
measure_theory.ae_eq_fun.pos_part
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[has_zero γ]
(f : α →ₘ[μ] γ) :
Positive part of an ae_eq_fun.
Equations
- f.pos_part = measure_theory.ae_eq_fun.comp (λ (x : γ), linear_order.max x 0) measure_theory.ae_eq_fun.pos_part._proof_1 f
@[simp]
theorem
measure_theory.ae_eq_fun.pos_part_mk
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[has_zero γ]
(f : α → γ)
(hf : measure_theory.ae_strongly_measurable f μ) :
(measure_theory.ae_eq_fun.mk f hf).pos_part = measure_theory.ae_eq_fun.mk (λ (x : α), linear_order.max (f x) 0) _
theorem
measure_theory.ae_eq_fun.coe_fn_pos_part
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
[has_zero γ]
(f : α →ₘ[μ] γ) :
def
continuous_map.to_ae_eq_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[second_countable_topology_either α β]
[topological_space.pseudo_metrizable_space β]
(f : C(α, β)) :
The equivalence class of μ-almost-everywhere measurable functions associated to a continuous
map.
Equations
theorem
continuous_map.coe_fn_to_ae_eq_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[second_countable_topology_either α β]
[topological_space.pseudo_metrizable_space β]
(f : C(α, β)) :
⇑(continuous_map.to_ae_eq_fun μ f) =ᵐ[μ] ⇑f
def
continuous_map.to_ae_eq_fun_add_hom
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[second_countable_topology_either α β]
[topological_space.pseudo_metrizable_space β]
[add_group β]
[topological_add_group β] :
The add_hom from the group of continuous maps from α to β to the group of
equivalence classes of μ-almost-everywhere measurable functions.
Equations
- continuous_map.to_ae_eq_fun_add_hom μ = {to_fun := continuous_map.to_ae_eq_fun μ _inst_6, map_zero' := _, map_add' := _}
def
continuous_map.to_ae_eq_fun_mul_hom
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
[topological_space β]
[second_countable_topology_either α β]
[topological_space.pseudo_metrizable_space β]
[group β]
[topological_group β] :
The mul_hom from the group of continuous maps from α to β to the group of equivalence
classes of μ-almost-everywhere measurable functions.
Equations
- continuous_map.to_ae_eq_fun_mul_hom μ = {to_fun := continuous_map.to_ae_eq_fun μ _inst_6, map_one' := _, map_mul' := _}
def
continuous_map.to_ae_eq_fun_linear_map
{α : Type u_1}
{γ : Type u_3}
[measurable_space α]
(μ : measure_theory.measure α)
[topological_space α]
[borel_space α]
{𝕜 : Type u_5}
[semiring 𝕜]
[topological_space γ]
[topological_space.pseudo_metrizable_space γ]
[add_comm_group γ]
[module 𝕜 γ]
[topological_add_group γ]
[has_continuous_const_smul 𝕜 γ]
[second_countable_topology_either α γ] :
The linear map from the group of continuous maps from α to β to the group of equivalence
classes of μ-almost-everywhere measurable functions.
Equations
- continuous_map.to_ae_eq_fun_linear_map μ = {to_fun := (continuous_map.to_ae_eq_fun_add_hom μ).to_fun, map_add' := _, map_smul' := _}