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 space.

Notation #

Main statements #

Implementation notes #

Tags #

function space, almost everywhere equal, L⁰, ae_eq_fun

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

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

    Instances For

      The space of equivalence classes of almost everywhere strongly measurable functions, where two strongly measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

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

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

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

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

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

            A measurable representative of an AEEqFun [f]

            @[simp]
            theorem MeasureTheory.AEEqFun.quot_mk_eq_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : αβ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
            Quot.mk Setoid.r { val := f, property := hf } = MeasureTheory.AEEqFun.mk f hf
            theorem MeasureTheory.AEEqFun.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
            f = g
            theorem MeasureTheory.AEEqFun.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
            theorem MeasureTheory.AEEqFun.induction_on {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop} (H : (f : αβ) → (hf : MeasureTheory.AEStronglyMeasurable f μ) → p (MeasureTheory.AEEqFun.mk f hf)) :
            p f
            theorem MeasureTheory.AEEqFun.induction_on₂ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {α' : Type u_5} {β' : Type u_6} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : MeasureTheory.Measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop} (H : (f : αβ) → (hf : MeasureTheory.AEStronglyMeasurable f μ) → (f' : α'β') → (hf' : MeasureTheory.AEStronglyMeasurable f' μ') → p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf')) :
            p f f'
            theorem MeasureTheory.AEEqFun.induction_on₃ {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {α' : Type u_5} {β' : Type u_6} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : MeasureTheory.Measure α'} {α'' : Type u_7} {β'' : Type u_8} [MeasurableSpace α''] [TopologicalSpace β''] {μ'' : MeasureTheory.Measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop} (H : (f : αβ) → (hf : MeasureTheory.AEStronglyMeasurable f μ) → (f' : α'β') → (hf' : MeasureTheory.AEStronglyMeasurable f' μ') → (f'' : α''β'') → (hf'' : MeasureTheory.AEStronglyMeasurable f'' μ'') → p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf') (MeasureTheory.AEEqFun.mk f'' hf'')) :
            p f f' f''

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

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

            See also AEEqFun.compMeasurePreserving.

            Instances For
              def MeasureTheory.AEEqFun.compMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] γ) (f : αβ) (hf : MeasureTheory.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.

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

                Instances For
                  @[simp]
                  theorem MeasureTheory.AEEqFun.comp_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : βγ) (hg : Continuous g) (f : αβ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                  theorem MeasureTheory.AEEqFun.comp_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : βγ) (hg : Continuous g) (f : α →ₘ[μ] β) :
                  theorem MeasureTheory.AEEqFun.coeFn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : βγ) (hg : Continuous 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.

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

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

                    Instances For
                      @[simp]
                      theorem MeasureTheory.AEEqFun.pair_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
                      MeasureTheory.AEEqFun.pair f g = MeasureTheory.AEEqFun.mk (fun x => (f x, g x)) (_ : MeasureTheory.AEStronglyMeasurable (fun x => (f x, g x)) μ)
                      theorem MeasureTheory.AEEqFun.coeFn_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
                      ↑(MeasureTheory.AEEqFun.pair f g) =ᶠ[MeasureTheory.Measure.ae μ] fun x => (f x, g x)
                      def MeasureTheory.AEEqFun.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.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)] : α →ₘ γ

                      Instances For
                        @[simp]
                        theorem MeasureTheory.AEEqFun.comp₂_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (g : βγδ) (hg : Continuous (Function.uncurry g)) (f₁ : αβ) (f₂ : αγ) (hf₁ : MeasureTheory.AEStronglyMeasurable f₁ μ) (hf₂ : MeasureTheory.AEStronglyMeasurable f₂ μ) :
                        MeasureTheory.AEEqFun.comp₂ g hg (MeasureTheory.AEEqFun.mk f₁ hf₁) (MeasureTheory.AEEqFun.mk f₂ hf₂) = MeasureTheory.AEEqFun.mk (fun a => g (f₁ a) (f₂ a)) (_ : MeasureTheory.AEStronglyMeasurable (fun x => Function.uncurry g (f₁ x, f₂ x)) μ)
                        theorem MeasureTheory.AEEqFun.comp₂_eq_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (g : βγδ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
                        theorem MeasureTheory.AEEqFun.comp₂_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (g : βγδ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
                        MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.mk (fun a => g (f₁ a) (f₂ a)) (_ : MeasureTheory.AEStronglyMeasurable (fun x => Function.uncurry g (f₁ x, f₂ x)) μ)
                        theorem MeasureTheory.AEEqFun.coeFn_comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (g : βγδ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
                        ↑(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂) =ᶠ[MeasureTheory.Measure.ae μ] fun a => g (f₁ a) (f₂ a)

                        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.

                        Instances For

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

                          Instances For
                            theorem MeasureTheory.AEEqFun.toGerm_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] :
                            Function.Injective MeasureTheory.AEEqFun.toGerm
                            def MeasureTheory.AEEqFun.LiftPred {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.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

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

                              Instances For
                                theorem MeasureTheory.AEEqFun.liftRel_mk_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {r : βγProp} {f : αβ} {g : αγ} {hf : MeasureTheory.AEStronglyMeasurable f μ} {hg : MeasureTheory.AEStronglyMeasurable g μ} :
                                MeasureTheory.AEEqFun.LiftRel r (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {r : βγProp} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
                                MeasureTheory.AEEqFun.LiftRel r f g ∀ᵐ (a : α) ∂μ, r (f a) (g a)
                                @[simp]
                                theorem MeasureTheory.AEEqFun.coeFn_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Preorder β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
                                theorem MeasureTheory.AEEqFun.coeFn_sup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                ↑(f g) =ᶠ[MeasureTheory.Measure.ae μ] fun x => f x g x
                                theorem MeasureTheory.AEEqFun.le_sup_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                f f g
                                theorem MeasureTheory.AEEqFun.le_sup_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                g f g
                                theorem MeasureTheory.AEEqFun.sup_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) (f' : α →ₘ[μ] β) (hf : f f') (hg : g f') :
                                f g f'
                                theorem MeasureTheory.AEEqFun.coeFn_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                ↑(f g) =ᶠ[MeasureTheory.Measure.ae μ] fun x => f x g x
                                theorem MeasureTheory.AEEqFun.inf_le_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                f g f
                                theorem MeasureTheory.AEEqFun.inf_le_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                f g g
                                theorem MeasureTheory.AEEqFun.le_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f' : α →ₘ[μ] β) (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) (hf : f' f) (hg : f' g) :
                                f' f g
                                def MeasureTheory.AEEqFun.const (α : Type u_1) {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (b : β) :
                                α →ₘ[μ] β

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

                                Instances For
                                  instance MeasureTheory.AEEqFun.instZero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Zero β] :
                                  Zero (α →ₘ[μ] β)
                                  instance MeasureTheory.AEEqFun.instOne {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [One β] :
                                  One (α →ₘ[μ] β)
                                  instance MeasureTheory.AEEqFun.instSMul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                  SMul 𝕜 (α →ₘ[μ] γ)
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.smul_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : αγ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                                  theorem MeasureTheory.AEEqFun.coeFn_smul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
                                  theorem MeasureTheory.AEEqFun.smul_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ) :
                                  instance MeasureTheory.AEEqFun.instSMulCommClass {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.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 α] {μ : MeasureTheory.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜ᵐᵒᵖ γ] [IsCentralScalar 𝕜 γ] :
                                  IsCentralScalar 𝕜 (α →ₘ[μ] γ)
                                  theorem MeasureTheory.AEEqFun.coeFn_add {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  ↑(f + g) =ᶠ[MeasureTheory.Measure.ae μ] f + g
                                  theorem MeasureTheory.AEEqFun.coeFn_mul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  ↑(f * g) =ᶠ[MeasureTheory.Measure.ae μ] f * g
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.coeFn_pow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ) :
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.toGermAddMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) :
                                  MeasureTheory.AEEqFun.toGermAddMonoidHom f = MeasureTheory.AEEqFun.toGerm f
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.toGermMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) :
                                  MeasureTheory.AEEqFun.toGermMonoidHom f = MeasureTheory.AEEqFun.toGerm f
                                  theorem MeasureTheory.AEEqFun.coeFn_sub {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  ↑(f - g) =ᶠ[MeasureTheory.Measure.ae μ] f - g
                                  theorem MeasureTheory.AEEqFun.coeFn_div {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  ↑(f / g) =ᶠ[MeasureTheory.Measure.ae μ] f / g
                                  theorem MeasureTheory.AEEqFun.coeFn_zpow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ) :
                                  instance MeasureTheory.AEEqFun.instMulAction {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Monoid 𝕜] [MulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                  MulAction 𝕜 (α →ₘ[μ] γ)
                                  instance MeasureTheory.AEEqFun.instModule {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Semiring 𝕜] [AddCommMonoid γ] [ContinuousAdd γ] [Module 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                  Module 𝕜 (α →ₘ[μ] γ)

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

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

                                    Positive part of an AEEqFun.

                                    Instances For

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

                                      Instances For

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

                                        Instances For

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

                                          Instances For

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

                                            Instances For