awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hσ : ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have neg : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) 0 fun (x : Ω) ↦
  HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: rw [condLExp_of_not_sigmaFinite bot_le hσ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : IsFiniteMeasure P
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have pos : ∀ (c : ℝ≥0∞) (h_eq : P⁻[X|⊥] = fun (x : Ω) ↦ c),
  P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: obtain ⟨c, h_eq⟩ := eq_const_of_measurable_bot (measurable_condLExp ⊥ P X)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : IsFiniteMeasure P
c : ℝ≥0∞
h_eq : P⁻[X|⊥] = fun (x : Ω) ↦ c
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have pos : ∀ (x : Ω), P⁻[X|⊥] x = HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: ext _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : IsFiniteMeasure P
c : ℝ≥0∞
h_eq : P⁻[X|⊥] = fun (x : Ω) ↦ c
x : Ω
⊢ P⁻[X|⊥] x = HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have pos : P⁻[X|⊥] x = HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), P⁻[X|⊥] ω ∂P)
Tactic: rw [← lintegral_condLExp bot_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
⊢ P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have inl : condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
  HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)
Tactic: rcases eq_zero_or_neZero P with rfl | hP
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
inl :
  condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)
⊢ P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have inr : ∀ (hP : NeZero P),
  P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: rcases eq_zero_or_neZero P with rfl | hP
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
⊢ condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)
have inl : condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[⊥] fun (x : Ω) ↦
  HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)
Tactic: rw [ae_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have neg : (ae P).EventuallyLE (β := ℝ≥0∞) 0 0
Tactic: simp_rw [condLExp_of_not_le hm, Filter.EventuallyLE.rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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)
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have neg : (ae P).EventuallyLE (β := ℝ≥0∞) 0 0
Tactic: simp_rw [condLExp_of_not_sigmaFinite hm hσ, Filter.EventuallyLE.rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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)
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
have pos : P⁻[X|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[Y|mΩ]
Tactic: apply ae_le_of_ae_le_trim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[Y|mΩ] x ∂P.trim hm
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[Y|mΩ] x ∂P.trim hm
Tactic: rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[Y|mΩ] x ∂P.trim hm
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P
Tactic: rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[Y|mΩ] x ∂P.trim hm
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P
Tactic: repeat rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P
have pos : ∀ᵐ (x : Ω) ∂P, x ∈ s → X x ≤ Y x
Tactic: apply setLIntegral_mono_ae' (hm s hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : Ω) ∂P, x ∈ s → X x ≤ Y x
have 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
Tactic: filter_upwards [hXY] using fun _ h _ ↦ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∀ᵐ (x : Ω) ∂P, x ∈ s → X x ≤ Y x
have h₁ : ∀ (a : Ω), X a ≤ Y a → a ∈ s → X a ≤ Y a
Tactic: filter_upwards [hXY] using fun _ h _ ↦ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have neg : HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
Tactic: simp_rw [condLExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
have neg : ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have neg : HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
Tactic: simp_rw [condLExp_of_not_sigmaFinite hm hσ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0 ≤ᶠ[ae P] 0
have neg : ∀ (a : Ω), HAdd.hAdd (α := Ω → ℝ≥0∞) (β := Ω → ℝ≥0∞) 0 0 a ≤ 0 a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]
have pos : P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[X + Y|mΩ]
Tactic: apply ae_le_of_ae_le_trim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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∞)
⊢ ∫⁻ (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
have 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
Tactic: rw [lintegral_add_left (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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, 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
have 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
Tactic: rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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∞)
⊢ ∫⁻ (ω : Ω) 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
have pos : ∫⁻ (ω : Ω) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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∞)
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y|mΩ] x ∂P.trim hm
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
Tactic: rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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, 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
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
Tactic: repeat rw [setLIntegral_condLExp_trim hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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∞)
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
have pos : ∫⁻ (a : Ω) in s, X a + Y a ∂P ≤ ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
Tactic: grw [le_lintegral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have neg : 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0
Tactic: simp_rw [condLExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have neg : 0 =ᶠ[ae P] HAdd.hAdd (α := Ω → ℝ≥0∞) 0 0
Tactic: simp_rw [condLExp_of_not_sigmaFinite hm hσ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (P⁻[X|mΩ] + P⁻[Y|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (X + Y) ω ∂P
Tactic: refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω + P⁻[Y|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
have pos : ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
Tactic: rw [lintegral_add_left (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
Tactic: rw [setLIntegral_condLExp hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
Tactic: rw [setLIntegral_condLExp hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (a : Ω) in s, P⁻[X|mΩ] a ∂P + ∫⁻ (a : Ω) in s, P⁻[Y|mΩ] a ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
Tactic: repeat rw [setLIntegral_condLExp hm _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω + Y ω ∂P
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P + ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (a : Ω) in s, X a ∂P + ∫⁻ (a : Ω) in s, Y a ∂P
Tactic: rw [lintegral_add_left' (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hY : AEMeasurable Y P
⊢ P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]
have rw : P⁻[Y + X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ] + P⁻[X|mΩ]
Tactic: rw [add_comm, add_comm P⁻[X|mΩ]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hm : mΩ ≤ mΩ₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
⊢ P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]
Tactic: by_cases hσ : SigmaFinite (P.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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Ω]
have pos : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, (c • P⁻[X|mΩ]) ω ∂P = ∫⁻ (ω : Ω) in s, (c • X) ω ∂P
Tactic: refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
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
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
have pos : AEMeasurable X (P.restrict s)
Tactic: rw [lintegral_const_mul, lintegral_const_mul'', setLIntegral_condLExp _ _ _ hs]