Conditional expectation in L1

This file contains two more steps of the construction of the conditional expectation, which is completed in MeasureTheory.Function.ConditionalExpectation.Basic. See that file for a description of the full process.

The conditional expectation of an L² function is defined in MeasureTheory.Function.ConditionalExpectation.CondexpL2. In this file, we perform two steps.

• Show that the conditional expectation of the indicator of a measurable set with finite measure is integrable and define a map Set α → (E →L[ℝ] (α →₁[μ] E)) which to a set associates a linear map. That linear map sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condExpL1CLM : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file MeasureTheory/Integral/SetToL1).

Main definitions

• condExpL1: Conditional expectation of a function as a linear map from L1 to itself.

Conditional expectation of an indicator as a continuous linear map.

The goal of this section is to build condExpInd (hm : m ≤ m0) (μ : Measure α) (s : Set s) : G →L[ℝ] α →₁[μ] G, which takes x : G to the conditional expectation of the indicator of the set s with value x, seen as an element of α →₁[μ] G.

def MeasureTheory.condExpIndL1Fin {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↥(Lp G 1 μ)

Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.

@[deprecated MeasureTheory.condExpIndL1Fin (since := "2025-01-21")]

def MeasureTheory.condexpIndL1Fin {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↥(Lp G 1 μ)

Alias of MeasureTheory.condExpIndL1Fin.

---

Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.

theorem MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↑↑(condExpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)

theorem MeasureTheory.condExpIndL1Fin_add {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G) : condExpIndL1Fin hm hs hμs (x + y) = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y

@[deprecated MeasureTheory.condExpIndL1Fin_add (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1Fin_add {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G) : condExpIndL1Fin hm hs hμs (x + y) = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y

Alias of MeasureTheory.condExpIndL1Fin_add.

theorem MeasureTheory.condExpIndL1Fin_smul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : ℝ) (x : G) : condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

@[deprecated MeasureTheory.condExpIndL1Fin_smul (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1Fin_smul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : ℝ) (x : G) : condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Alias of MeasureTheory.condExpIndL1Fin_smul.

theorem MeasureTheory.condExpIndL1Fin_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F) : condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

@[deprecated MeasureTheory.condExpIndL1Fin_smul' (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1Fin_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F) : condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Alias of MeasureTheory.condExpIndL1Fin_smul'.

theorem MeasureTheory.norm_condExpIndL1Fin_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ‖condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖x‖

@[deprecated MeasureTheory.norm_condExpIndL1Fin_le (since := "2025-01-21")]

theorem MeasureTheory.norm_condexpIndL1Fin_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ‖condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖x‖

Alias of MeasureTheory.norm_condExpIndL1Fin_le.

theorem MeasureTheory.condExpIndL1Fin_disjoint_union {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) (x : G) : condExpIndL1Fin hm ⋯ ⋯ x = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

def MeasureTheory.condExpIndL1 {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) (s : Set α) [SigmaFinite (μ.trim hm)] (x : G) : ↥(Lp G 1 μ)

Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.

@[deprecated MeasureTheory.condExpIndL1 (since := "2025-01-21")]

def MeasureTheory.condexpIndL1 {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) (s : Set α) [SigmaFinite (μ.trim hm)] (x : G) : ↥(Lp G 1 μ)

Alias of MeasureTheory.condExpIndL1.

---

Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.

theorem MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : condExpIndL1 hm μ s x = condExpIndL1Fin hm hs hμs x

@[deprecated MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1_of_measurableSet_of_measure_ne_top {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : condExpIndL1 hm μ s x = condExpIndL1Fin hm hs hμs x

Alias of MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top.

theorem MeasureTheory.condExpIndL1_of_measure_eq_top {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hμs : μ s = ⊤) (x : G) : condExpIndL1 hm μ s x = 0

theorem MeasureTheory.condExpIndL1_of_not_measurableSet {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : ¬MeasurableSet s) (x : G) : condExpIndL1 hm μ s x = 0

theorem MeasureTheory.condExpIndL1_add {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x y : G) : condExpIndL1 hm μ s (x + y) = condExpIndL1 hm μ s x + condExpIndL1 hm μ s y

@[deprecated MeasureTheory.condExpIndL1_add (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1_add {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x y : G) : condExpIndL1 hm μ s (x + y) = condExpIndL1 hm μ s x + condExpIndL1 hm μ s y

Alias of MeasureTheory.condExpIndL1_add.

theorem MeasureTheory.condExpIndL1_smul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : ℝ) (x : G) : condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

@[deprecated MeasureTheory.condExpIndL1_smul (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1_smul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : ℝ) (x : G) : condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

Alias of MeasureTheory.condExpIndL1_smul.

theorem MeasureTheory.condExpIndL1_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) : condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

@[deprecated MeasureTheory.condExpIndL1_smul' (since := "2025-01-21")]

theorem MeasureTheory.condexpIndL1_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) : condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

Alias of MeasureTheory.condExpIndL1_smul'.

theorem MeasureTheory.norm_condExpIndL1_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x : G) : ‖condExpIndL1 hm μ s x‖ ≤ μ.real s * ‖x‖

@[deprecated MeasureTheory.norm_condExpIndL1_le (since := "2025-01-21")]

theorem MeasureTheory.norm_condexpIndL1_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x : G) : ‖condExpIndL1 hm μ s x‖ ≤ μ.real s * ‖x‖

Alias of MeasureTheory.norm_condExpIndL1_le.

theorem MeasureTheory.continuous_condExpIndL1 {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : Continuous fun (x : G) => condExpIndL1 hm μ s x

@[deprecated MeasureTheory.continuous_condExpIndL1 (since := "2025-01-21")]

theorem MeasureTheory.continuous_condexpIndL1 {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : Continuous fun (x : G) => condExpIndL1 hm μ s x

Alias of MeasureTheory.continuous_condExpIndL1.

theorem MeasureTheory.condExpIndL1_disjoint_union {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) (x : G) : condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

def MeasureTheory.condExpInd {α : Type u_1} (G : Type u_4) [NormedAddCommGroup G] [NormedSpace ℝ G] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (s : Set α) : G →L[ℝ] ↥(Lp G 1 μ)

Conditional expectation of the indicator of a set, as a linear map from G to L1.

@[deprecated MeasureTheory.condExpInd (since := "2025-01-21")]

def MeasureTheory.condexpInd {α : Type u_1} (G : Type u_4) [NormedAddCommGroup G] [NormedSpace ℝ G] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (s : Set α) : G →L[ℝ] ↥(Lp G 1 μ)

Alias of MeasureTheory.condExpInd.

---

Conditional expectation of the indicator of a set, as a linear map from G to L1.

theorem MeasureTheory.condExpInd_ae_eq_condExpIndSMul {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↑↑((condExpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)

theorem MeasureTheory.aestronglyMeasurable_condExpInd {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : AEStronglyMeasurable (↑↑((condExpInd G hm μ s) x)) μ

@[deprecated MeasureTheory.aestronglyMeasurable_condExpInd (since := "2025-01-21")]

theorem MeasureTheory.aestronglyMeasurable'_condexpInd {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : AEStronglyMeasurable (↑↑((condExpInd G hm μ s) x)) μ

Alias of MeasureTheory.aestronglyMeasurable_condExpInd.

@[simp]

theorem MeasureTheory.condExpInd_empty {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : condExpInd G hm μ ∅ = 0

@[deprecated MeasureTheory.condExpInd_empty (since := "2025-01-21")]

theorem MeasureTheory.condexpInd_empty {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : condExpInd G hm μ ∅ = 0

Alias of MeasureTheory.condExpInd_empty.

theorem MeasureTheory.condExpInd_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) : (condExpInd F hm μ s) (c • x) = c • (condExpInd F hm μ s) x

@[deprecated MeasureTheory.condExpInd_smul' (since := "2025-01-21")]

theorem MeasureTheory.condexpInd_smul' {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) : (condExpInd F hm μ s) (c • x) = c • (condExpInd F hm μ s) x

Alias of MeasureTheory.condExpInd_smul'.

theorem MeasureTheory.norm_condExpInd_apply_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x : G) : ‖(condExpInd G hm μ s) x‖ ≤ μ.real s * ‖x‖

@[deprecated MeasureTheory.norm_condExpInd_apply_le (since := "2025-01-21")]

theorem MeasureTheory.norm_condexpInd_apply_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (x : G) : ‖(condExpInd G hm μ s) x‖ ≤ μ.real s * ‖x‖

Alias of MeasureTheory.norm_condExpInd_apply_le.

theorem MeasureTheory.norm_condExpInd_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : ‖condExpInd G hm μ s‖ ≤ μ.real s

@[deprecated MeasureTheory.norm_condExpInd_le (since := "2025-01-21")]

theorem MeasureTheory.norm_condexpInd_le {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : ‖condExpInd G hm μ s‖ ≤ μ.real s

Alias of MeasureTheory.norm_condExpInd_le.

theorem MeasureTheory.condExpInd_disjoint_union_apply {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) (x : G) : (condExpInd G hm μ (s ∪ t)) x = (condExpInd G hm μ s) x + (condExpInd G hm μ t) x

theorem MeasureTheory.condExpInd_disjoint_union {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) : condExpInd G hm μ (s ∪ t) = condExpInd G hm μ s + condExpInd G hm μ t

@[deprecated MeasureTheory.condExpInd_disjoint_union (since := "2025-01-21")]

theorem MeasureTheory.condexpInd_disjoint_union {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) : condExpInd G hm μ (s ∪ t) = condExpInd G hm μ s + condExpInd G hm μ t

Alias of MeasureTheory.condExpInd_disjoint_union.

theorem MeasureTheory.dominatedFinMeasAdditive_condExpInd {α : Type u_1} (G : Type u_4) [NormedAddCommGroup G] {m m0 : MeasurableSpace α} [NormedSpace ℝ G] (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] : DominatedFinMeasAdditive μ (condExpInd G hm μ) 1

theorem MeasureTheory.setIntegral_condExpInd {α : Type u_1} {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G'] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (x : G') : ∫ (a : α) in s, ↑↑((condExpInd G' hm μ t) x) a ∂μ = μ.real (t ∩ s) • x

@[deprecated MeasureTheory.setIntegral_condExpInd (since := "2025-01-21")]

theorem MeasureTheory.setIntegral_condexpInd {α : Type u_1} {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G'] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (x : G') : ∫ (a : α) in s, ↑↑((condExpInd G' hm μ t) x) a ∂μ = μ.real (t ∩ s) • x

Alias of MeasureTheory.setIntegral_condExpInd.

theorem MeasureTheory.condExpInd_of_measurable {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : G) : (condExpInd G hm μ s) c = indicatorConstLp 1 ⋯ hμs c

@[deprecated MeasureTheory.condExpInd_of_measurable (since := "2025-01-21")]

theorem MeasureTheory.condexpInd_of_measurable {α : Type u_1} {G : Type u_4} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : G) : (condExpInd G hm μ s) c = indicatorConstLp 1 ⋯ hμs c

Alias of MeasureTheory.condExpInd_of_measurable.

theorem MeasureTheory.condExpInd_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {E : Type u_7} [NormedAddCommGroup E] [PartialOrder E] [NormedSpace ℝ E] [OrderedSMul ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) (hx : 0 ≤ x) : 0 ≤ (condExpInd E hm μ s) x

@[deprecated MeasureTheory.condExpInd_nonneg (since := "2025-01-21")]

theorem MeasureTheory.condexpInd_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {E : Type u_7} [NormedAddCommGroup E] [PartialOrder E] [NormedSpace ℝ E] [OrderedSMul ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) (hx : 0 ≤ x) : 0 ≤ (condExpInd E hm μ s) x

Alias of MeasureTheory.condExpInd_nonneg.

def MeasureTheory.condExpL1CLM {α : Type u_1} (F' : Type u_3) [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] : ↥(Lp F' 1 μ) →L[ℝ] ↥(Lp F' 1 μ)

Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.

@[deprecated MeasureTheory.condExpL1CLM (since := "2025-01-21")]

def MeasureTheory.condexpL1CLM {α : Type u_1} (F' : Type u_3) [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] : ↥(Lp F' 1 μ) →L[ℝ] ↥(Lp F' 1 μ)

Alias of MeasureTheory.condExpL1CLM.

---

Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.

theorem MeasureTheory.condExpL1CLM_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : 𝕜) (f : ↥(Lp F' 1 μ)) : (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

@[deprecated MeasureTheory.condExpL1CLM_smul (since := "2025-01-21")]

theorem MeasureTheory.condexpL1CLM_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : 𝕜) (f : ↥(Lp F' 1 μ)) : (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

Alias of MeasureTheory.condExpL1CLM_smul.

theorem MeasureTheory.condExpL1CLM_indicatorConstLp {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F') : (condExpL1CLM F' hm μ) (indicatorConstLp 1 hs hμs x) = (condExpInd F' hm μ s) x

theorem MeasureTheory.condExpL1CLM_indicatorConst {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F') : (condExpL1CLM F' hm μ) ↑(Lp.simpleFunc.indicatorConst 1 hs hμs x) = (condExpInd F' hm μ s) x

theorem MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Set α} (f : ↥(Lp F' 1 μ)) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Auxiliary lemma used in the proof of setIntegral_condExpL1CLM.

theorem MeasureTheory.setIntegral_condExpL1CLM {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Set α} (f : ↥(Lp F' 1 μ)) (hs : MeasurableSet s) : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

The integral of the conditional expectation condExpL1CLM over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condExp, the similar statement for condExp.

theorem MeasureTheory.aestronglyMeasurable_condExpL1CLM {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : ↥(Lp F' 1 μ)) : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ

@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1CLM (since := "2025-01-21")]

theorem MeasureTheory.aestronglyMeasurable_condexpL1CLM {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : ↥(Lp F' 1 μ)) : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ

Alias of MeasureTheory.aestronglyMeasurable_condExpL1CLM.

theorem MeasureTheory.condExpL1CLM_lpMeas {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : ↥(lpMeas F' ℝ m 1 μ)) : (condExpL1CLM F' hm μ) ↑f = ↑f

@[deprecated MeasureTheory.condExpL1CLM_lpMeas (since := "2025-01-21")]

theorem MeasureTheory.condexpL1CLM_lpMeas {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : ↥(lpMeas F' ℝ m 1 μ)) : (condExpL1CLM F' hm μ) ↑f = ↑f

Alias of MeasureTheory.condExpL1CLM_lpMeas.

theorem MeasureTheory.condExpL1CLM_of_aestronglyMeasurable' {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : ↥(Lp F' 1 μ)) (hfm : AEStronglyMeasurable (↑↑f) μ) : (condExpL1CLM F' hm μ) f = f

def MeasureTheory.condExpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (f : α → F') : ↥(Lp F' 1 μ)

Conditional expectation of a function, in L1. Its value is 0 if the function is not integrable. The function-valued condExp should be used instead in most cases.

@[deprecated MeasureTheory.condExpL1 (since := "2025-01-21")]

def MeasureTheory.condexpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (f : α → F') : ↥(Lp F' 1 μ)

Alias of MeasureTheory.condExpL1.

---

Conditional expectation of a function, in L1. Its value is 0 if the function is not integrable. The function-valued condExp should be used instead in most cases.

theorem MeasureTheory.condExpL1_undef {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} (hf : ¬Integrable f μ) : condExpL1 hm μ f = 0

@[deprecated MeasureTheory.condExpL1_undef (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_undef {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} (hf : ¬Integrable f μ) : condExpL1 hm μ f = 0

Alias of MeasureTheory.condExpL1_undef.

theorem MeasureTheory.condExpL1_eq {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} (hf : Integrable f μ) : condExpL1 hm μ f = (condExpL1CLM F' hm μ) (Integrable.toL1 f hf)

@[deprecated MeasureTheory.condExpL1_eq (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_eq {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} (hf : Integrable f μ) : condExpL1 hm μ f = (condExpL1CLM F' hm μ) (Integrable.toL1 f hf)

Alias of MeasureTheory.condExpL1_eq.

@[simp]

theorem MeasureTheory.condExpL1_zero {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : condExpL1 hm μ 0 = 0

@[deprecated MeasureTheory.condExpL1_zero (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_zero {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] : condExpL1 hm μ 0 = 0

Alias of MeasureTheory.condExpL1_zero.

@[simp]

theorem MeasureTheory.condExpL1_measure_zero {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {f : α → F'} (hm : m ≤ m0) : condExpL1 hm 0 f = 0

@[deprecated MeasureTheory.condExpL1_measure_zero (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_measure_zero {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {f : α → F'} (hm : m ≤ m0) : condExpL1 hm 0 f = 0

Alias of MeasureTheory.condExpL1_measure_zero.

theorem MeasureTheory.aestronglyMeasurable_condExpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} : AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

@[deprecated MeasureTheory.aestronglyMeasurable_condExpL1 (since := "2025-01-21")]

theorem MeasureTheory.aestronglyMeasurable_condexpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} : AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Alias of MeasureTheory.aestronglyMeasurable_condExpL1.

theorem MeasureTheory.condExpL1_congr_ae {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {f g : α → F'} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (h : f =ᶠ[ae μ] g) : condExpL1 hm μ f = condExpL1 hm μ g

@[deprecated MeasureTheory.condExpL1_congr_ae (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_congr_ae {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {f g : α → F'} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (h : f =ᶠ[ae μ] g) : condExpL1 hm μ f = condExpL1 hm μ g

Alias of MeasureTheory.condExpL1_congr_ae.

theorem MeasureTheory.integrable_condExpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : α → F') : Integrable (↑↑(condExpL1 hm μ f)) μ

@[deprecated MeasureTheory.integrable_condExpL1 (since := "2025-01-21")]

theorem MeasureTheory.integrable_condexpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : α → F') : Integrable (↑↑(condExpL1 hm μ f)) μ

Alias of MeasureTheory.integrable_condExpL1.

theorem MeasureTheory.setIntegral_condExpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} {s : Set α} (hf : Integrable f μ) (hs : MeasurableSet s) : ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

The integral of the conditional expectation condExpL1 over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condExp, the similar statement for condExp.

@[deprecated MeasureTheory.setIntegral_condExpL1 (since := "2025-01-21")]

theorem MeasureTheory.setIntegral_condexpL1 {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} {s : Set α} (hf : Integrable f μ) (hs : MeasurableSet s) : ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

Alias of MeasureTheory.setIntegral_condExpL1.

---

The integral of the conditional expectation condExpL1 over an m-measurable set is equal to the integral of f on that set. See also setIntegral_condExp, the similar statement for condExp.

theorem MeasureTheory.condExpL1_add {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f g : α → F'} (hf : Integrable f μ) (hg : Integrable g μ) : condExpL1 hm μ (f + g) = condExpL1 hm μ f + condExpL1 hm μ g

@[deprecated MeasureTheory.condExpL1_add (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_add {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f g : α → F'} (hf : Integrable f μ) (hg : Integrable g μ) : condExpL1 hm μ (f + g) = condExpL1 hm μ f + condExpL1 hm μ g

Alias of MeasureTheory.condExpL1_add.

theorem MeasureTheory.condExpL1_neg {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : α → F') : condExpL1 hm μ (-f) = -condExpL1 hm μ f

@[deprecated MeasureTheory.condExpL1_neg (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_neg {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (f : α → F') : condExpL1 hm μ (-f) = -condExpL1 hm μ f

Alias of MeasureTheory.condExpL1_neg.

theorem MeasureTheory.condExpL1_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : 𝕜) (f : α → F') : condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

@[deprecated MeasureTheory.condExpL1_smul (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [RCLike 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] (c : 𝕜) (f : α → F') : condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

Alias of MeasureTheory.condExpL1_smul.

theorem MeasureTheory.condExpL1_sub {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f g : α → F'} (hf : Integrable f μ) (hg : Integrable g μ) : condExpL1 hm μ (f - g) = condExpL1 hm μ f - condExpL1 hm μ g

@[deprecated MeasureTheory.condExpL1_sub (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_sub {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f g : α → F'} (hf : Integrable f μ) (hg : Integrable g μ) : condExpL1 hm μ (f - g) = condExpL1 hm μ f - condExpL1 hm μ g

Alias of MeasureTheory.condExpL1_sub.

theorem MeasureTheory.condExpL1_of_aestronglyMeasurable' {α : Type u_1} {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {f : α → F'} (hfm : AEStronglyMeasurable f μ) (hfi : Integrable f μ) : ↑↑(condExpL1 hm μ f) =ᶠ[ae μ] f

theorem MeasureTheory.condExpL1_mono {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {E : Type u_7} [NormedAddCommGroup E] [PartialOrder E] [OrderClosedTopology E] [IsOrderedAddMonoid E] [CompleteSpace E] [NormedSpace ℝ E] [OrderedSMul ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᶠ[ae μ] g) : ↑↑(condExpL1 hm μ f) ≤ᶠ[ae μ] ↑↑(condExpL1 hm μ g)

@[deprecated MeasureTheory.condExpL1_mono (since := "2025-01-21")]

theorem MeasureTheory.condexpL1_mono {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {E : Type u_7} [NormedAddCommGroup E] [PartialOrder E] [OrderClosedTopology E] [IsOrderedAddMonoid E] [CompleteSpace E] [NormedSpace ℝ E] [OrderedSMul ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᶠ[ae μ] g) : ↑↑(condExpL1 hm μ f) ≤ᶠ[ae μ] ↑↑(condExpL1 hm μ g)

Alias of MeasureTheory.condExpL1_mono.