awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm_not : ¬mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] = 0
have rw : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞)
  (if hm : mΩ ≤ mΩ₀ then
    if SigmaFinite (P.trim hm) then if Measurable X then X else ∂(P.withDensity X).trim hm/∂P.trim hm else 0
  else 0)
  0
Tactic: rw [condLExp, dif_neg hm_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm_not : ¬mΩ ≤ mΩ₀
rw :
  Eq.{u_1 + 1} (α := Ω → ℝ≥0∞)
    (if hm : mΩ ≤ mΩ₀ then
      if SigmaFinite (P.trim hm) then if Measurable X then X else ∂(P.withDensity X).trim hm/∂P.trim hm else 0
    else 0)
    0
⊢ P⁻[X|mΩ] = 0
have rw₁ : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) 0 0
Tactic: rw [condLExp, dif_neg hm_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
⊢ Measurable P⁻[X|mΩ]
have pos : ∀ (hm : mΩ ≤ mΩ₀), Measurable 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∞
pos : ∀ (hm : mΩ ≤ mΩ₀), Measurable P⁻[X|mΩ]
⊢ Measurable P⁻[X|mΩ]
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), Measurable 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∞
hm : mΩ ≤ mΩ₀
⊢ Measurable P⁻[X|mΩ]
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), Measurable 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∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), Measurable P⁻[X|mΩ]
⊢ Measurable P⁻[X|mΩ]
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), Measurable 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∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable P⁻[X|mΩ]
have pos : ∀ (hX : Measurable X), Measurable P⁻[X|mΩ]
Tactic: by_cases hX : Measurable[mΩ] X
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : ∀ (hX : Measurable X), Measurable P⁻[X|mΩ]
⊢ Measurable P⁻[X|mΩ]
have neg : ∀ (hX : ¬Measurable X), Measurable P⁻[X|mΩ]
Tactic: by_cases hX : Measurable[mΩ] X
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have pos : ∀ (hX : Measurable X), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: by_cases hX : Measurable[mΩ] X
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
pos : ∀ (hX : Measurable X), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg : ∀ (hX : ¬Measurable X), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: by_cases hX : Measurable[mΩ] X
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (hypothesis)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have h : (P.withDensity X).trim hm ≪ P.trim hm
Tactic: have h := AbsolutelyContinuous.trim (withDensity_absolutelyContinuous P X) hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (hypothesis)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have this : SFinite ((P.withDensity X).trim hm)
Tactic: have : SFinite ((P.withDensity X).trim hm) := sFinite_of_absolutelyContinuous h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₂ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₂ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₃ : ∫⁻ (a : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₂ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₃ : ∫⁻ (a : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₄ : ((P.withDensity X).trim hm : (a : Set Ω) → ℝ≥0∞) s = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₂ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₃ : ∫⁻ (a : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₄ : ((P.withDensity X).trim hm : (a : Set Ω) → ℝ≥0∞) s = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₅ : (P.withDensity X : (a : Set Ω) → ℝ≥0∞) s = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
neg : ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₁ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₂ : ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₃ : ∫⁻ (a : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₄ : ((P.withDensity X).trim hm : (a : Set Ω) → ℝ≥0∞) s = ∫⁻ (ω : Ω) in s, X ω ∂P
neg₅ : (P.withDensity X : (a : Set Ω) → ℝ≥0∞) s = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
have neg₆ : ∫⁻ (a : Ω) in s, X a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [condLExp_of_not_sub_sigma_measurable hm _ hX, ← lintegral_indicator (hm s hs),
    ← lintegral_trim hm (by measurability), lintegral_indicator hs, setLIntegral_rnDeriv' h hs,
    trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
have rw : ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [setLIntegral_trim hm (measurable_condLExp _ _ _) hs, setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
rw : ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
have rw₁ : ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [setLIntegral_trim hm (measurable_condLExp _ _ _) hs, setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
have pos : ∀ (hm : mΩ ≤ mΩ₀), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
pos : ∀ (hm : mΩ ≤ mΩ₀), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x ≠ ∞
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ P⁻[f|mΩ] x < ∞) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ P⁻[f|mΩ] x ≠ ∞) x} x}
    a
Tactic: filter_upwards [condLExp_lt_top hf] with x hx using hx.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ P⁻[f|mΩ] x < ∞) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ P⁻[f|mΩ] x ≠ ∞) x} x}
      a
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x ≠ ∞
have h₁ : ∀ (a : Ω), P⁻[f|mΩ] a < ∞ → P⁻[f|mΩ] a ≠ ∞
Tactic: filter_upwards [condLExp_lt_top hf] with x hx using hx.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ Y =ᶠ[ae P] P⁻[X|mΩ]
have h12 : Y =ᶠ[ae (P.trim hm)] P⁻[X|mΩ]
Tactic: apply ae_eq_of_ae_eq_trim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, Y x ∂P.trim hm = ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm
have h12 : ∫⁻ (x : Ω) in s, Y x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Tactic: rw [setLIntegral_trim_ae hm hY hs, setLIntegral_condLExp_trim _ _ _ 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
⊢ 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 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 pos : ∀ (s : Set Ω) (hs : MeasurableSet s), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
Tactic: refine ae_eq_condLExp _ _ _ (measurable_condLExp _ _ _) (fun 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
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
have pos : ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
Tactic: rw [setLIntegral_condLExp _ _ _ 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
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
have pos : ∀ᵐ (x : Ω) ∂P, x ∈ s → X x = Y x
Tactic: apply setLIntegral_congr_fun_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
⊢ ∀ᵐ (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] with _ h _ using 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 :
  ∀ (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] with _ h _ using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
⊢ P⁻[0|mΩ] = 0
have pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[0|mΩ] = 0
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 Ω
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[0|mΩ] = 0
⊢ P⁻[0|mΩ] = 0
have neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[0|mΩ] = 0
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 Ω
hm : mΩ ≤ mΩ₀
⊢ P⁻[0|mΩ] = 0
have pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[0|mΩ] = 0
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 Ω
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[0|mΩ] = 0
⊢ P⁻[0|mΩ] = 0
have neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[0|mΩ] = 0
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 Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᶠ[ae P] Y
⊢ P⁻[X|mΩ] =ᶠ[ae (P.trim hm)] P⁻[Y|mΩ]
have apply : P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]
Tactic: apply ae_eq_trim_of_measurable hm (measurable_condLExp _ _ X) (measurable_condLExp _ _ Y)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have pos : ∀ (hP : IsFiniteMeasure P),
  P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: by_cases hP : IsFiniteMeasure P
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (goal)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
pos :
  ∀ (hP : IsFiniteMeasure P),
    P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have neg : ∀ (hP : ¬IsFiniteMeasure P),
  P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
Tactic: by_cases hP : IsFiniteMeasure P
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (hypothesis)
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 hσ : ¬SigmaFinite (m0 := ⊥) (P.trim sorry)
Tactic: have hσ : ¬SigmaFinite (P.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalLExpectation (hypothesis)
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
hσ : ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)
⊢ P⁻[X|⊥] = fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)
have hP₁ : Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [not_isFiniteMeasure_iff] at hP
Cleared hypotheses: hP, hσ