Documentation

Mathlib.MeasureTheory.Integral.SetToL1

Extension of a linear function from indicators to L1 #

Let T : Set α → E →L[ℝ] F be additive for measurable sets with finite measure, in the sense that for s, t two such sets, s ∩ t = ∅ → T (s ∪ t) = T s + T t. T is akin to a bilinear map on Set α × E, or a linear map on indicator functions.

This file constructs an extension of T to integrable simple functions, which are finite sums of indicators of measurable sets with finite measure, then to integrable functions, which are limits of integrable simple functions.

The main result is a continuous linear map (α →₁[μ] E) →L[ℝ] F. This extension process is used to define the Bochner integral in the MeasureTheory.Integral.Bochner file and the conditional expectation of an integrable function in MeasureTheory.Function.ConditionalExpectation.

Main Definitions #

Properties #

For most properties of setToFun, we provide two lemmas. One version uses hypotheses valid on all sets, like T = T', and a second version which uses a primed name uses hypotheses on measurable sets with finite measure, like ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s.

The lemmas listed here don't show all hypotheses. Refer to the actual lemmas for details.

Linearity:

Other:

If the space is a NormedLatticeAddCommGroup and T is such that 0 ≤ T s x for 0 ≤ x, we also prove order-related properties:

Implementation notes #

The starting object T : Set α → E →L[ℝ] F matters only through its restriction on measurable sets with finite measure. Its value on other sets is ignored.

def MeasureTheory.FinMeasAdditive {α : Type u_1} {β : Type u_7} [AddMonoid β] :
{x : MeasurableSpace α} → MeasureTheory.Measure α(Set αβ)Prop

A set function is FinMeasAdditive if its value on the union of two disjoint measurable sets with finite measure is the sum of its values on each set.

Equations
Instances For
    theorem MeasureTheory.FinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} {T' : Set αβ} (hT : MeasureTheory.FinMeasAdditive μ T) (hT' : MeasureTheory.FinMeasAdditive μ T') :
    theorem MeasureTheory.FinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} [Monoid 𝕜] [DistribMulAction 𝕜 β] (hT : MeasureTheory.FinMeasAdditive μ T) (c : 𝕜) :
    MeasureTheory.FinMeasAdditive μ fun (s : Set α) => c T s
    theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} {μ' : MeasureTheory.Measure α} (h : ∀ (s : Set α), MeasurableSet sμ s = μ' s = ) (hT : MeasureTheory.FinMeasAdditive μ T) :
    theorem MeasureTheory.FinMeasAdditive.of_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} (c : ENNReal) (hc_ne_top : c ) (hT : MeasureTheory.FinMeasAdditive (c μ) T) :
    theorem MeasureTheory.FinMeasAdditive.smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} (c : ENNReal) (hc_ne_zero : c 0) (hT : MeasureTheory.FinMeasAdditive μ T) :
    theorem MeasureTheory.FinMeasAdditive.smul_measure_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] {T : Set αβ} (c : ENNReal) (hc_ne_zero : c 0) (hc_ne_top : c ) :
    theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddCommMonoid β] (T : Set αβ) (T_empty : T = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) {ι : Type u_8} (S : ιSet α) (sι : Finset ι) (hS_meas : ∀ (i : ι), MeasurableSet (S i)) (hSp : i, μ (S i) ) (h_disj : i, j, i jDisjoint (S i) (S j)) :
    T (⋃ i ∈ , S i) = Finset.sum fun (i : ι) => T (S i)
    def MeasureTheory.DominatedFinMeasAdditive {α : Type u_1} {β : Type u_7} [SeminormedAddCommGroup β] :
    {x : MeasurableSpace α} → MeasureTheory.Measure α(Set αβ)Prop

    A FinMeasAdditive set function whose norm on every set is less than the measure of the set (up to a multiplicative constant).

    Equations
    Instances For
      theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [NormedAddCommGroup β] {T : Set αβ} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hs_zero : μ s = 0) :
      T s = 0
      theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero {α : Type u_1} {β : Type u_8} [NormedAddCommGroup β] {T : Set αβ} {C : } {m : MeasurableSpace α} (hT : MeasureTheory.DominatedFinMeasAdditive 0 T C) {s : Set α} (hs : MeasurableSet s) :
      T s = 0
      theorem MeasureTheory.DominatedFinMeasAdditive.add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set αβ} {T' : Set αβ} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') :
      theorem MeasureTheory.DominatedFinMeasAdditive.smul {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set αβ} {C : } [NormedField 𝕜] [NormedSpace 𝕜 β] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (c : 𝕜) :
      MeasureTheory.DominatedFinMeasAdditive μ (fun (s : Set α) => c T s) (c * C)
      theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [SeminormedAddCommGroup β] {T : Set αβ} {C : } {μ' : MeasureTheory.Measure α} (c : ENNReal) (hc : c ) (h : μ c μ') (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hC : 0 C) :

      Extend Set α → (F →L[ℝ] F') to (α →ₛ F) → F'.

      Equations
      Instances For
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F'] [NormedSpace F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F'} (h_zero : ∀ (s : Set α), MeasurableSet sμ s < T s = 0) (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (f) μ) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left' {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F'] [NormedSpace F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F') (T' : Set αE →L[] F') (c : ) (h_smul : ∀ (s : Set α), MeasurableSet sμ s < T' s = c T s) {f : MeasureTheory.SimpleFunc α E} (hf : MeasureTheory.Integrable (f) μ) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [NormedAddCommGroup E] [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace E] [NormedSpace 𝕜 F] (T : Set αE →L[] F) (h_add : MeasureTheory.FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) {f : MeasureTheory.SimpleFunc α E} (hf : MeasureTheory.Integrable (f) μ) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] {m : MeasurableSpace α} (T : Set αF →L[] G'') (T' : Set αF →L[] G'') (hTT' : ∀ (s : Set α) (x : F), (T s) x (T' s) x) (f : MeasureTheory.SimpleFunc α F) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] (T : Set αE →L[] G'') (T' : Set αE →L[] G'') (hTT' : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : E), (T s) x (T' s) x) (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (f) μ) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {m : MeasurableSpace α} (T : Set αG' →L[] G'') (hT_nonneg : ∀ (s : Set α) (x : G'), 0 x0 (T s) x) (f : MeasureTheory.SimpleFunc α G') (hf : 0 f) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] (T : Set αG' →L[] G'') (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) (f : MeasureTheory.SimpleFunc α G') (hf : 0 f) (hfi : MeasureTheory.Integrable (f) μ) :
        theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} (h_add : MeasureTheory.FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : MeasureTheory.SimpleFunc α G'} {g : MeasureTheory.SimpleFunc α G'} (hfi : MeasureTheory.Integrable (f) μ) (hgi : MeasureTheory.Integrable (g) μ) (hfg : f g) :
        @[deprecated MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm]

        Alias of MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm.

        theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm {α : Type u_1} {F : Type u_3} {F' : Type u_4} [NormedAddCommGroup F] [NormedSpace F] [NormedAddCommGroup F'] [NormedSpace F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αF →L[] F') {C : } (hT_norm : ∀ (s : Set α), MeasurableSet sT s C * (μ s).toReal) (f : MeasureTheory.SimpleFunc α F) :
        theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable {α : Type u_1} {E : Type u_2} {F' : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F'] [NormedSpace F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F') {C : } (hT_norm : ∀ (s : Set α), MeasurableSet sμ s < T s C * (μ s).toReal) (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (f) μ) :

        Extend Set α → (E →L[ℝ] F') to (α →₁ₛ[μ] E) → F'.

        Equations
        Instances For
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), MeasurableSet sμ s < T s = 0) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F) (T' : Set αE →L[] F) (h : ∀ (s : Set α), MeasurableSet sμ s < T s = T' s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :

          setToL1S does not change if we replace the measure μ by μ' with μ ≪ μ'. The statement uses two functions f and f' because they have to belong to different types, but morally these are the same function (we have f =ᵐ[μ] f').

          theorem MeasureTheory.L1.SimpleFunc.setToL1S_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F) (T' : Set αE →L[] F) (T'' : Set αE →L[] F) (h_add : ∀ (s : Set α), MeasurableSet sμ s < T'' s = T s + T' s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F) (T' : Set αE →L[] F) (c : ) (h_smul : ∀ (s : Set α), MeasurableSet sμ s < T' s = c T s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_real {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (c : ) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedField 𝕜] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace E] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (T : Set αE →L[] F) (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.norm_setToL1S_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set αE →L[] F) {C : } (hT_norm : ∀ (s : Set α), MeasurableSet sμ s < T s C * (μ s).toReal) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} {s : Set α} (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (hs : MeasurableSet s) (hμs : μ s < ) (x : E) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {T : Set αE →L[] F} (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (x : E) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} (hTT' : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} {G' : Type u_8} [NormedLatticeAddCommGroup G'] [NormedSpace G'] [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αG'' →L[] G'} (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G''), 0 x0 (T s) x) {f : (MeasureTheory.Lp.simpleFunc G'' 1 μ)} (hf : 0 f) :
          theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} {G' : Type u_8} [NormedLatticeAddCommGroup G'] [NormedSpace G'] [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αG'' →L[] G'} (h_zero : ∀ (s : Set α), MeasurableSet sμ s = 0T s = 0) (h_add : MeasureTheory.FinMeasAdditive μ T) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G''), 0 x0 (T s) x) {f : (MeasureTheory.Lp.simpleFunc G'' 1 μ)} {g : (MeasureTheory.Lp.simpleFunc G'' 1 μ)} (hfg : f g) :
          def MeasureTheory.L1.SimpleFunc.setToL1SCLM' (α : Type u_1) (E : Type u_2) {F : Type u_3} (𝕜 : Type u_6) [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) :

          Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[𝕜] F.

          Equations
          Instances For

            Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[ℝ] F.

            Equations
            Instances For
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet sμ s < T s = 0) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet sμ s < T s = T' s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet sμ s < T'' s = T s + T' s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (c : ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h_smul : ∀ (s : Set α), MeasurableSet sμ s < T' s = c T s) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp.simpleFunc E 1 μ)) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp.simpleFunc G' 1 μ)} (hf : 0 f) :
              theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp.simpleFunc G' 1 μ)} {g : (MeasureTheory.Lp.simpleFunc G' 1 μ)} (hfg : f g) :
              def MeasureTheory.L1.setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) :
              (MeasureTheory.Lp E 1 μ) →L[𝕜] F

              Extend set α → (E →L[ℝ] F) to (α →₁[μ] E) →L[𝕜] F.

              Equations
              Instances For

                Extend Set α → E →L[ℝ] F to (α →₁[μ] E) →L[ℝ] F.

                Equations
                Instances For
                  theorem MeasureTheory.L1.setToL1_eq_setToL1' {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet sμ s < T s = 0) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] (T : Set αE →L[] F) (T' : Set αE →L[] F) {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h : T = T') (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] (T : Set αE →L[] F) (T' : Set αE →L[] F) {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet sμ s < T s = T' s) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet sμ s < T'' s = T s + T' s) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (c : ) (h_smul : ∀ (s : Set α), MeasurableSet sμ s < T' s = c T s) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_simpleFunc_indicatorConst {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ) (x : E) :
                  theorem MeasureTheory.L1.setToL1_indicatorConstLp {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (x : E) :
                  theorem MeasureTheory.L1.setToL1_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp E 1 μ)) :
                  theorem MeasureTheory.L1.setToL1_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp G' 1 μ)} (hf : 0 f) :
                  theorem MeasureTheory.L1.setToL1_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : (MeasureTheory.Lp G' 1 μ)} {g : (MeasureTheory.Lp G' 1 μ)} (hfg : f g) :
                  theorem MeasureTheory.L1.tendsto_setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : (MeasureTheory.Lp E 1 μ)) {ι : Type u_7} (fs : ι(MeasureTheory.Lp E 1 μ)) {l : Filter ι} (hfs : Filter.Tendsto fs l (nhds f)) :
                  Filter.Tendsto (fun (i : ι) => (MeasureTheory.L1.setToL1 hT) (fs i)) l (nhds ((MeasureTheory.L1.setToL1 hT) f))

                  If fs i → f in L1, then setToL1 hT (fs i) → setToL1 hT f.

                  def MeasureTheory.setToFun {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [CompleteSpace F] (T : Set αE →L[] F) {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : αE) :
                  F

                  Extend T : Set α → E →L[ℝ] F to (α → E) → F (for integrable functions α → E). We set it to 0 if the function is not integrable.

                  Equations
                  Instances For
                    theorem MeasureTheory.setToFun_undef {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hf : ¬MeasureTheory.Integrable f μ) :
                    theorem MeasureTheory.setToFun_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h : T = T') (f : αE) :
                    theorem MeasureTheory.setToFun_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet sμ s < T s = T' s) (f : αE) :
                    theorem MeasureTheory.setToFun_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (f : αE) :
                    theorem MeasureTheory.setToFun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {T'' : Set αE →L[] F} {C : } {C' : } {C'' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet sμ s < T'' s = T s + T' s) (f : αE) :
                    theorem MeasureTheory.setToFun_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (c : ) (f : αE) :
                    MeasureTheory.setToFun μ (fun (s : Set α) => c T s) f = c MeasureTheory.setToFun μ T hT f
                    theorem MeasureTheory.setToFun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {T' : Set αE →L[] F} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (c : ) (h_smul : ∀ (s : Set α), MeasurableSet sμ s < T' s = c T s) (f : αE) :
                    theorem MeasureTheory.setToFun_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet sμ s < T s = 0) :
                    theorem MeasureTheory.setToFun_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                    theorem MeasureTheory.setToFun_finset_sum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι) {f : ιαE} (hf : is, MeasureTheory.Integrable (f i) μ) :
                    MeasureTheory.setToFun μ T hT (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => MeasureTheory.setToFun μ T hT (f i)
                    theorem MeasureTheory.setToFun_finset_sum {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι) {f : ιαE} (hf : is, MeasureTheory.Integrable (f i) μ) :
                    (MeasureTheory.setToFun μ T hT fun (a : α) => Finset.sum s fun (i : ι) => f i a) = Finset.sum s fun (i : ι) => MeasureTheory.setToFun μ T hT (f i)
                    theorem MeasureTheory.setToFun_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : αE) :
                    theorem MeasureTheory.setToFun_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
                    theorem MeasureTheory.setToFun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c x) = c (T s) x) (c : 𝕜) (f : αE) :
                    theorem MeasureTheory.setToFun_congr_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} {g : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
                    theorem MeasureTheory.setToFun_measure_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h : μ = 0) :
                    theorem MeasureTheory.setToFun_measure_zero' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {f : αE} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (h : ∀ (s : Set α), MeasurableSet sμ s < μ s = 0) :
                    theorem MeasureTheory.setToFun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (x : E) :
                    MeasureTheory.setToFun μ T hT (Set.indicator s fun (x_1 : α) => x) = (T s) x
                    theorem MeasureTheory.setToFun_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (x : E) :
                    (MeasureTheory.setToFun μ T hT fun (x_1 : α) => x) = (T Set.univ) x
                    theorem MeasureTheory.setToFun_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : E), (T s) x (T' s) x) (f : αE) :
                    theorem MeasureTheory.setToFun_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] {T : Set αE →L[] G''} {T' : Set αE →L[] G''} {C : } {C' : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x (T' s) x) (f : (MeasureTheory.Lp E 1 μ)) :
                    MeasureTheory.setToFun μ T hT f MeasureTheory.setToFun μ T' hT' f
                    theorem MeasureTheory.setToFun_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : αG'} (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] f) :
                    theorem MeasureTheory.setToFun_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8} [NormedLatticeAddCommGroup G''] [NormedSpace G''] [CompleteSpace G''] [NormedLatticeAddCommGroup G'] [NormedSpace G'] {T : Set αG' →L[] G''} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet sμ s < ∀ (x : G'), 0 x0 (T s) x) {f : αG'} {g : αG'} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᶠ[MeasureTheory.Measure.ae μ] g) :
                    theorem MeasureTheory.tendsto_setToFun_of_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (f : αE) (hfi : MeasureTheory.Integrable f μ) {fs : ιαE} {l : Filter ι} (hfsi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ) (hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), fs i x - f x‖₊μ) l (nhds 0)) :
                    Filter.Tendsto (fun (i : ι) => MeasureTheory.setToFun μ T hT (fs i)) l (nhds (MeasureTheory.setToFun μ T hT f))

                    If F i → f in L1, then setToFun μ T hT (F i) → setToFun μ T hT f.

                    theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) [MeasurableSpace E] [BorelSpace E] {f : αE} {s : Set E} [TopologicalSpace.SeparableSpace s] (hfi : MeasureTheory.Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ (x : α) ∂μ, f x closure s) {y₀ : E} (h₀ : y₀ s) (h₀i : MeasureTheory.Integrable (fun (x : α) => y₀) μ) :
                    Filter.Tendsto (fun (n : ) => MeasureTheory.setToFun μ T hT (MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (nhds (MeasureTheory.setToFun μ T hT f))
                    theorem MeasureTheory.continuous_L1_toL1 {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {μ' : MeasureTheory.Measure α} (c' : ENNReal) (hc' : c' ) (hμ'_le : μ' c' μ) :
                    Continuous fun (f : (MeasureTheory.Lp G 1 μ)) => MeasureTheory.Integrable.toL1 f

                    Auxiliary lemma for setToFun_congr_measure: the function sending f : α →₁[μ] G to f : α →₁[μ'] G is continuous when μ' ≤ c' • μ for c' ≠ ∞.

                    theorem MeasureTheory.setToFun_congr_measure_of_integrable {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {C' : } {μ' : MeasureTheory.Measure α} (c' : ENNReal) (hc' : c' ) (hμ'_le : μ' c' μ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C') (f : αE) (hfμ : MeasureTheory.Integrable f μ) :
                    theorem MeasureTheory.setToFun_congr_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {C' : } {μ' : MeasureTheory.Measure α} (c : ENNReal) (c' : ENNReal) (hc : c ) (hc' : c' ) (hμ_le : μ c μ') (hμ'_le : μ' c' μ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C') (f : αE) :
                    theorem MeasureTheory.setToFun_congr_measure_of_add_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {C' : } {μ' : MeasureTheory.Measure α} (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : αE) (hf : MeasureTheory.Integrable f (μ + μ')) :
                    MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ T hT f
                    theorem MeasureTheory.setToFun_congr_measure_of_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {C' : } {μ' : MeasureTheory.Measure α} (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : MeasureTheory.DominatedFinMeasAdditive μ' T C) (f : αE) (hf : MeasureTheory.Integrable f (μ + μ')) :
                    MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ' T hT f
                    theorem MeasureTheory.setToFun_congr_smul_measure {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {C' : } (c : ENNReal) (hc_ne_top : c ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_smul : MeasureTheory.DominatedFinMeasAdditive (c μ) T C') (f : αE) :
                    MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun (c μ) T hT_smul f
                    theorem MeasureTheory.tendsto_setToFun_of_dominated_convergence {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : αE} {f : αE} (bound : α) (fs_measurable : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (fs n) μ) (bound_integrable : MeasureTheory.Integrable bound μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, fs n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => fs n a) Filter.atTop (nhds (f a))) :
                    Filter.Tendsto (fun (n : ) => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop (nhds (MeasureTheory.setToFun μ T hT f))

                    Lebesgue dominated convergence theorem provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their image by setToFun. We could weaken the condition bound_integrable to require HasFiniteIntegral bound μ instead (i.e. not requiring that bound is measurable), but in all applications proving integrability is easier.

                    theorem MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} {l : Filter ι} [Filter.IsCountablyGenerated l] {fs : ιαE} {f : αE} (bound : α) (hfs_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (fs n) μ) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, fs n a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => fs n a) l (nhds (f a))) :
                    Filter.Tendsto (fun (n : ι) => MeasureTheory.setToFun μ T hT (fs n)) l (nhds (MeasureTheory.setToFun μ T hT f))

                    Lebesgue dominated convergence theorem for filters with a countable basis

                    theorem MeasureTheory.continuousWithinAt_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : XαE} {x₀ : X} {bound : α} {s : Set X} (hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (fs x) μ) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀) :
                    ContinuousWithinAt (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) s x₀
                    theorem MeasureTheory.continuousAt_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : XαE} {x₀ : X} {bound : α} (hfs_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fs x) μ) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀) :
                    ContinuousAt (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) x₀
                    theorem MeasureTheory.continuousOn_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : XαE} {bound : α} {s : Set X} (hfs_meas : xs, MeasureTheory.AEStronglyMeasurable (fs x) μ) (h_bound : xs, ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s) :
                    ContinuousOn (fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)) s
                    theorem MeasureTheory.continuous_setToFun_of_dominated {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteSpace F] {T : Set αE →L[] F} {C : } {X : Type u_7} [TopologicalSpace X] [FirstCountableTopology X] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : XαE} {bound : α} (hfs_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (fs x) μ) (h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, fs x a bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a) :
                    Continuous fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)