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.

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

    Equations
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def MeasureTheory.AEEqFun.mk {α : Type u_1} [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.

        Equations
        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. We ensure that if f has a constant representative, then we choose that one.

          Equations
          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]

            Equations
            • MeasureTheory.AEEqFun.instCoeFun = { coe := MeasureTheory.AEEqFun.cast }
            @[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 f, hf = MeasureTheory.AEEqFun.mk f hf
            @[simp]
            theorem MeasureTheory.AEEqFun.mk_coeFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) :
            theorem MeasureTheory.AEEqFun.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
            f = g f =ᵐ[μ] g
            theorem MeasureTheory.AEEqFun.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) :
            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.

            Equations
            Instances For
              @[simp]
              theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} {g : βγ} (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) :
              (MeasureTheory.AEEqFun.mk g hg).compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
              theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} (g : β →ₘ[ν] γ) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) :
              g.compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
              theorem MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} (g : β →ₘ[ν] γ) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) :
              (g.compQuasiMeasurePreserving f hf) =ᵐ[μ] g f
              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.

              Equations
              • g.compMeasurePreserving f hf = g.compQuasiMeasurePreserving f
              Instances For
                @[simp]
                theorem MeasureTheory.AEEqFun.compMeasurePreserving_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} {g : βγ} (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.MeasurePreserving f μ ν) :
                (MeasureTheory.AEEqFun.mk g hg).compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
                theorem MeasureTheory.AEEqFun.compMeasurePreserving_eq_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} (g : β →ₘ[ν] γ) (hf : MeasureTheory.MeasurePreserving f μ ν) :
                g.compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g f)
                theorem MeasureTheory.AEEqFun.coeFn_compMeasurePreserving {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : αβ} (g : β →ₘ[ν] γ) (hf : MeasureTheory.MeasurePreserving f μ ν) :
                (g.compMeasurePreserving f hf) =ᵐ[μ] g f
                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] : α →ₘ γ.

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

                  Given a measurable function g : β → γ, and an almost everywhere equal function [f] : α →ₘ β, return the equivalence class of g ∘ f, i.e., the almost everywhere equal function [g ∘ f] : α →ₘ γ. This requires that γ has a second countable topology.

                  Equations
                  Instances For
                    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).

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

                      Equations
                      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))
                        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))
                        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₂) =ᵐ[μ] 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.

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

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

                          Equations
                          Instances For
                            @[simp]
                            theorem MeasureTheory.AEEqFun.mk_toGerm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : αβ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                            (MeasureTheory.AEEqFun.mk f hf).toGerm = f
                            theorem MeasureTheory.AEEqFun.toGerm_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : α →ₘ[μ] β) :
                            f.toGerm = f
                            theorem MeasureTheory.AEEqFun.toGerm_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] :
                            Function.Injective MeasureTheory.AEEqFun.toGerm
                            @[simp]
                            theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {β : Type u_5} [MeasurableSpace β] {f : αβ} {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] γ) (hf : MeasureTheory.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {β : Type u_5} [MeasurableSpace β] {f : αβ} {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] γ) (hf : MeasureTheory.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] (g : βγ) (hg : Continuous g) (f : α →ₘ[μ] β) :
                            (MeasureTheory.AEEqFun.comp 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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : βγδ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
                            (MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.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

                            Equations
                            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

                              Equations
                              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)
                                Equations
                                • MeasureTheory.AEEqFun.instPreorder = Preorder.lift MeasureTheory.AEEqFun.toGerm
                                @[simp]
                                theorem MeasureTheory.AEEqFun.coeFn_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Preorder β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
                                f ≤ᵐ[μ] g f g
                                Equations
                                • MeasureTheory.AEEqFun.instPartialOrder = PartialOrder.lift MeasureTheory.AEEqFun.toGerm
                                Equations
                                theorem MeasureTheory.AEEqFun.coeFn_sup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                (f g) =ᵐ[μ] 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'
                                Equations
                                theorem MeasureTheory.AEEqFun.coeFn_inf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : α →ₘ[μ] β) (g : α →ₘ[μ] β) :
                                (f g) =ᵐ[μ] 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
                                Equations
                                • MeasureTheory.AEEqFun.instLattice = Lattice.mk
                                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

                                Equations
                                Instances For
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.coeFn_const_eq (α : Type u_1) {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [NeZero μ] (b : β) (x : α) :

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

                                  Equations
                                  instance MeasureTheory.AEEqFun.instZero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Zero β] :
                                  Zero (α →ₘ[μ] β)
                                  Equations
                                  instance MeasureTheory.AEEqFun.instOne {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [One β] :
                                  One (α →ₘ[μ] β)
                                  Equations
                                  theorem MeasureTheory.AEEqFun.zero_def {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Zero β] :
                                  0 = MeasureTheory.AEEqFun.mk (fun (x : α) => 0)
                                  theorem MeasureTheory.AEEqFun.one_def {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [One β] :
                                  1 = MeasureTheory.AEEqFun.mk (fun (x : α) => 1)
                                  theorem MeasureTheory.AEEqFun.coeFn_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Zero β] :
                                  0 =ᵐ[μ] 0
                                  theorem MeasureTheory.AEEqFun.coeFn_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [One β] :
                                  1 =ᵐ[μ] 1
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.coeFn_zero_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [NeZero μ] [Zero β] {x : α} :
                                  0 x = 0
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.coeFn_one_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [NeZero μ] [One β] {x : α} :
                                  1 x = 1
                                  instance MeasureTheory.AEEqFun.instSMul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                  SMul 𝕜 (α →ₘ[μ] γ)
                                  Equations
                                  @[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 : α →ₘ[μ] γ) :
                                  (c f) =ᵐ[μ] c f
                                  theorem MeasureTheory.AEEqFun.smul_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} {𝕜' : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜' γ] [ContinuousConstSMul 𝕜' γ] [SMulCommClass 𝕜 𝕜' γ] :
                                  SMulCommClass 𝕜 𝕜' (α →ₘ[μ] γ)
                                  Equations
                                  • =
                                  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 𝕜 𝕜' (α →ₘ[μ] γ)
                                  Equations
                                  • =
                                  instance MeasureTheory.AEEqFun.instIsCentralScalar {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜ᵐᵒᵖ γ] [IsCentralScalar 𝕜 γ] :
                                  IsCentralScalar 𝕜 (α →ₘ[μ] γ)
                                  Equations
                                  • =
                                  instance MeasureTheory.AEEqFun.instAdd {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] :
                                  Add (α →ₘ[μ] γ)
                                  Equations
                                  instance MeasureTheory.AEEqFun.instMul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] :
                                  Mul (α →ₘ[μ] γ)
                                  Equations
                                  theorem MeasureTheory.AEEqFun.coeFn_add {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  (f + g) =ᵐ[μ] f + g
                                  theorem MeasureTheory.AEEqFun.coeFn_mul {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  (f * g) =ᵐ[μ] f * g
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.add_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  (f + g).toGerm = f.toGerm + g.toGerm
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.mul_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                  (f * g).toGerm = f.toGerm * g.toGerm
                                  Equations
                                  Equations
                                  Equations
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.coeFn_pow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ) :
                                  (f ^ n) =ᵐ[μ] f ^ n
                                  @[simp]
                                  theorem MeasureTheory.AEEqFun.pow_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ) :
                                  (f ^ n).toGerm = f.toGerm ^ n
                                  Equations

                                  AEEqFun.toGerm as an AddMonoidHom.

                                  Equations
                                  • MeasureTheory.AEEqFun.toGermAddMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_zero' := , map_add' := }
                                  Instances For
                                    theorem MeasureTheory.AEEqFun.toGermAddMonoidHom.proof_2 {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                    (f + g).toGerm = f.toGerm + g.toGerm
                                    @[simp]
                                    theorem MeasureTheory.AEEqFun.toGermMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₘ[μ] γ) :
                                    MeasureTheory.AEEqFun.toGermMonoidHom f = f.toGerm
                                    @[simp]
                                    theorem MeasureTheory.AEEqFun.toGermAddMonoidHom_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : α →ₘ[μ] γ) :
                                    MeasureTheory.AEEqFun.toGermAddMonoidHom f = f.toGerm

                                    AEEqFun.toGerm as a MonoidHom.

                                    Equations
                                    • MeasureTheory.AEEqFun.toGermMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_one' := , map_mul' := }
                                    Instances For
                                      Equations
                                      Equations
                                      instance MeasureTheory.AEEqFun.instInv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] :
                                      Inv (α →ₘ[μ] γ)
                                      Equations
                                      theorem MeasureTheory.AEEqFun.coeFn_neg {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : α →ₘ[μ] γ) :
                                      (-f) =ᵐ[μ] -f
                                      theorem MeasureTheory.AEEqFun.coeFn_inv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) :
                                      f⁻¹ =ᵐ[μ] (↑f)⁻¹
                                      theorem MeasureTheory.AEEqFun.neg_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : α →ₘ[μ] γ) :
                                      (-f).toGerm = -f.toGerm
                                      theorem MeasureTheory.AEEqFun.inv_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) :
                                      f⁻¹.toGerm = f.toGerm⁻¹
                                      Equations
                                      theorem MeasureTheory.AEEqFun.instSub.proof_1 {γ : Type u_1} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] :
                                      Continuous fun (p : γ × γ) => p.1 - p.2
                                      instance MeasureTheory.AEEqFun.instDiv {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] :
                                      Div (α →ₘ[μ] γ)
                                      Equations
                                      theorem MeasureTheory.AEEqFun.coeFn_sub {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                      (f - g) =ᵐ[μ] f - g
                                      theorem MeasureTheory.AEEqFun.coeFn_div {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                      (f / g) =ᵐ[μ] f / g
                                      theorem MeasureTheory.AEEqFun.sub_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                      (f - g).toGerm = f.toGerm - g.toGerm
                                      theorem MeasureTheory.AEEqFun.div_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (g : α →ₘ[μ] γ) :
                                      (f / g).toGerm = f.toGerm / g.toGerm
                                      Equations
                                      theorem MeasureTheory.AEEqFun.coeFn_zpow {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ) :
                                      (f ^ n) =ᵐ[μ] f ^ n
                                      @[simp]
                                      theorem MeasureTheory.AEEqFun.zpow_toGerm {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ) :
                                      (f ^ n).toGerm = f.toGerm ^ n
                                      Equations
                                      Equations
                                      Equations
                                      Equations
                                      instance MeasureTheory.AEEqFun.instMulAction {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Monoid 𝕜] [MulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                      MulAction 𝕜 (α →ₘ[μ] γ)
                                      Equations
                                      instance MeasureTheory.AEEqFun.instDistribMulAction {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Monoid 𝕜] [AddMonoid γ] [ContinuousAdd γ] [DistribMulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                      DistribMulAction 𝕜 (α →ₘ[μ] γ)
                                      Equations
                                      instance MeasureTheory.AEEqFun.instModule {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] {𝕜 : Type u_5} [Semiring 𝕜] [AddCommMonoid γ] [ContinuousAdd γ] [Module 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
                                      Module 𝕜 (α →ₘ[μ] γ)
                                      Equations

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

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

                                        Positive part of an AEEqFun.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem MeasureTheory.AEEqFun.posPart_mk {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] [Zero γ] (f : αγ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                                          (MeasureTheory.AEEqFun.mk f hf).posPart = MeasureTheory.AEEqFun.mk (fun (x : α) => max (f x) 0)
                                          theorem MeasureTheory.AEEqFun.coeFn_posPart {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] [Zero γ] (f : α →ₘ[μ] γ) :
                                          f.posPart =ᵐ[μ] fun (a : α) => max (f a) 0

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

                                          Equations
                                          Instances For

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

                                            Equations
                                            Instances For

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

                                              Equations
                                              Instances For

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

                                                Equations
                                                Instances For