awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ x ∈ s → X x ≤ Y x) x} x}
      a
h₁ : ∀ (a : Ω), X a ≤ Y a → a ∈ s → X a ≤ Y a
⊢ ∀ᵐ (x : Ω) ∂P, x ∈ s → X x ≤ Y x

Tactic:
filter_upwards [hXY] using fun _ h _ ↦ h
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
neg : HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
neg : ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a
⊢ HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a
⊢ HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[X + Y|mΩ]
pos₁ : MeasurableSpace Ω
pos₂ : mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

Tactic:
apply ae_le_of_ae_le_trim

Premises used: MeasureTheory.ae_le_of_ae_le_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (P⁻[X|mΩ] + P⁻[Y|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos :
  LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : Ω) in s, (P⁻[X|mΩ] + P⁻[Y|mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm
⊢ LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : Ω) in s, (P⁻[X|mΩ] + P⁻[Y|mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable P⁻[X|mΩ]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P.trim hm + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P.trim hm ≤
    ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm
⊢ ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x + P⁻[Y|mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
rw [lintegral_add_left (by fun_prop)]

Premises used: MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P.trim hm + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P.trim hm ≤
    ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
rw [setLIntegral_condLExp_trim hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
rw [setLIntegral_condLExp_trim hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
rw [setLIntegral_condLExp_trim hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P.trim hm + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P.trim hm ≤
    ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm

Tactic:
repeat rw [setLIntegral_condLExp_trim hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (a : Ω) in s, X a + Y a ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P

Tactic:
grw [le_lintegral_add]

Premises used: MeasureTheory.le_lintegral_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : Ω) in s, X a + Y a ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : ¬mΩ ≤ mΩ₀
neg : 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : ¬mΩ ≤ mΩ₀
⊢ 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (P⁻[X|mΩ] + P⁻[Y|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (P⁻[X|mΩ] + P⁻[Y|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm

Premises used: MeasureTheory.ae_eq_condLExp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Measurable P⁻[X|mΩ]

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω + P⁻[Y|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P

Tactic:
rw [lintegral_add_left (by measurability)]

Premises used: MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P

Tactic:
rw [setLIntegral_condLExp hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P

Tactic:
rw [setLIntegral_condLExp hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P

Tactic:
repeat rw [setLIntegral_condLExp hm _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ AEMeasurable X (P.restrict s)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos pos₁ : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (a : Ω) in s, X a ∂P + ∫⁻ (a : Ω) in s, Y a ∂P
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P

Tactic:
rw [lintegral_add_left' (by fun_prop)]

Premises used: MeasureTheory.lintegral_add_left'
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hY : AEMeasurable Y P
rw : P⁻[Y + X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ] + P⁻[X|mΩ]
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

Tactic:
rw [add_comm, add_comm P⁻[X|mΩ]]

Premises used: add_comm, MeasureTheory.condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hY : AEMeasurable Y P
⊢ P⁻[Y + X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ] + P⁻[X|mΩ]

Tactic:
condLExp_add_left X hY

Premises used: MeasureTheory.condLExp_add_left
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hY : AEMeasurable Y P
⊢ P⁻[Y + X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ] + P⁻[X|mΩ]

Tactic:
exact condLExp_add_left X hY

Premises used: MeasureTheory.condLExp_add_left
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
simp [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
simp [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (c • P⁻[X|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (c • P⁻[X|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm

Premises used: MeasureTheory.ae_eq_condLExp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos : AEMeasurable X (P.restrict s)
pos₁ : Measurable P⁻[X|mΩ]
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P

Tactic:
rw [lintegral_const_mul, lintegral_const_mul'', setLIntegral_condLExp _ _ _ hs]

Premises used: MeasureTheory.lintegral_const_mul'', MeasureTheory.lintegral_const_mul, MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ AEMeasurable X (P.restrict s)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Measurable P⁻[X|mΩ]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
pos : ∀ (hm : mΩ ≤ mΩ₀), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
neg : HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm]

Premises used: MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
neg : ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a
⊢ HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a
⊢ HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 ≤ᶠ[ae P] 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ ∀ (a : Ω), HSMul.hSMul (β := Ω → ℝ≥0∞) c 0 a ≤ 0 a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : c • P⁻[X|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[c • X|mΩ]
pos₁ : MeasurableSpace Ω
pos₂ : mΩ ≤ mΩ₀
⊢ c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

Tactic:
apply ae_le_of_ae_le_trim

Premises used: MeasureTheory.ae_le_of_ae_le_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (c • P⁻[X|mΩ])

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
pos :
  LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : Ω) in s, (c • P⁻[X|mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[c • X|mΩ] x ∂P.trim hm
⊢ LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : Ω) in s, (c • P⁻[X|mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[c • X|mΩ] x ∂P.trim hm

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, (c • P⁻[X|mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[c • X|mΩ] x ∂P.trim hm

Tactic:
simp [setLIntegral_condLExp_trim _ _ _ hs, lintegral_const_mul _ (measurable_condLExp _ P X),
    lintegral_const_mul_le]

Premises used: MeasureTheory.lintegral_const_mul_le, MeasureTheory.measurable_condLExp, MeasureTheory.lintegral_const_mul, MeasureTheory.setLIntegral_condLExp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀