theorem MeasureTheory.tsub_add_cancel_of_eventuallyLE {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : Measure Ω} {X Y : Ω → ENNReal} (hYX : Y ≤ᵐ[P] X) : X - Y + Y =ᵐ[P] X

theorem MeasureTheory.condLExp_sub {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X Y : Ω → ENNReal} (hY : AEMeasurable Y P) (hYX : Y ≤ᵐ[P] X) (hY_ne_top : ∀ᵐ (ω : Ω) ∂P, P⁻[Y | mΩ] ω ≠ ⊤) : P⁻[X - Y | mΩ] =ᵐ[P] P⁻[X | mΩ] - P⁻[Y | mΩ]

theorem MeasureTheory.condLExp_condLExp_of_le {Ω : Type u_1} {mΩ₀ mΩ₁ mΩ₂ : MeasurableSpace Ω} (hm₁₂ : mΩ₁ ≤ mΩ₂) (hm₂ : mΩ₂ ≤ mΩ₀) (P : Measure Ω) [SigmaFinite (P.trim hm₂)] (X : Ω → ENNReal) : P⁻[P⁻[X | mΩ₂] | mΩ₁] =ᵐ[P] P⁻[X | mΩ₁]