awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
refine_1 :
  LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)

Tactic:
rw [Measure.restrict_restrict (hm _ h_meas_nonneg_g), Measure.restrict_restrict h_meas_nonneg_f,
      hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonneg_g hs)
        ((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
      ← Measure.restrict_restrict (hm _ h_meas_nonneg_g), ←
      Measure.restrict_restrict h_meas_nonneg_f]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_restrict, lt_top_iff_ne_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)

Tactic:
setIntegral_le_nonneg (hm _ h_meas_nonneg_g) hf hfi

Premises used: MeasureTheory.setIntegral_le_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)

Tactic:
exact setIntegral_le_nonneg (hm _ h_meas_nonneg_g) hf hfi

Premises used: MeasureTheory.setIntegral_le_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
refine_2 :
  LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, f x ∂μ.restrict s)
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s)

Tactic:
rw [Measure.restrict_restrict (hm _ h_meas_nonpos_g), Measure.restrict_restrict h_meas_nonpos_f,
      hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonpos_g hs)
        ((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
      ← Measure.restrict_restrict (hm _ h_meas_nonpos_g), ←
      Measure.restrict_restrict h_meas_nonpos_f]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_restrict, lt_top_iff_ne_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, f x ∂μ.restrict s)

Tactic:
setIntegral_nonpos_le (hm _ h_meas_nonpos_g) hf hfi

Premises used: MeasureTheory.setIntegral_nonpos_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, f x ∂μ.restrict s)

Tactic:
exact setIntegral_nonpos_le (hm _ h_meas_nonpos_g) hf hfi

Premises used: MeasureTheory.setIntegral_nonpos_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)
rw₁ : LE.le (α := ℝ) 0 (∫ (x : α) in s, ‖f x‖ ∂μ)
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ

Tactic:
rw [← ofReal_integral_norm_eq_lintegral_enorm hfi, ←
    ofReal_integral_norm_eq_lintegral_enorm hgi, ENNReal.ofReal_le_ofReal_iff]

Premises used: ENNReal.ofReal_le_ofReal_iff, MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)

Tactic:
integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs

Premises used: MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)

Tactic:
exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs

Premises used: MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, ‖f x‖ ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) 0 0
⊢ P⁻[X|mΩ] = 0

Tactic:
rw [condLExp, dif_neg hm_not]

Premises used: dif_neg, MeasureTheory.condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hμm_not : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X|mΩ] = 0

Tactic:
simp [condLExp, dif_pos hm, hμm_not]

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

Tactic:
simp [condLExp, hm, hσ, hX]

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

Tactic:
simp [condLExp, hm, hσ, hX]

Premises used: MeasureTheory.condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
pos : ∀ (hm : mΩ ≤ mΩ₀), Measurable P⁻[X|mΩ]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), Measurable P⁻[X|mΩ]
⊢ Measurable 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∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), Measurable P⁻[X|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), Measurable P⁻[X|mΩ]
⊢ Measurable 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∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
pos : ∀ (hX : Measurable X), Measurable P⁻[X|mΩ]
neg : ∀ (hX : ¬Measurable X), Measurable P⁻[X|mΩ]
⊢ Measurable P⁻[X|mΩ]

Tactic:
by_cases hX : Measurable[mΩ] X

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

Tactic:
simp [condLExp_eq_self hm, hX]

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

Tactic:
simp [condLExp_of_not_sub_sigma_measurable hm _ hX, measurable_rnDeriv]

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

Tactic:
simp [condLExp_of_not_sigmaFinite hm hσ, measurable_zero]

Premises used: measurable_zero, MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ Measurable P⁻[X|mΩ]

Tactic:
simp [condLExp_of_not_le hm, measurable_zero]

Premises used: MeasureTheory.condLExp_of_not_le, measurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
⊢ Measurable P⁻[X|mΩ]

Tactic:
(measurable_condLExp _ _ _).mono hm (le_refl _)

Premises used: le_refl, MeasureTheory.measurable_condLExp, Measurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
⊢ Measurable P⁻[X|mΩ]

Tactic:
exact (measurable_condLExp _ _ _).mono hm (le_refl _)

Premises used: le_refl, MeasureTheory.measurable_condLExp, Measurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
neg : ∀ (hX : ¬Measurable X), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
by_cases hX : Measurable[mΩ] X

Premises used: Measurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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

Tactic:
simp [condLExp_eq_self hm _ hX]

Premises used: MeasureTheory.condLExp_eq_self
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
⊢ (P.withDensity X).trim hm ≪ P.trim hm

Tactic:
have h := AbsolutelyContinuous.trim (withDensity_absolutelyContinuous P X) hm
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
⊢ SFinite ((P.withDensity X).trim hm)

Tactic:
have : SFinite ((P.withDensity X).trim hm) := sFinite_of_absolutelyContinuous h
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
⊢ Measurable (s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm))

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
neg₆ neg₇ : ∫⁻ (a : Ω) in s, X a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂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)]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv', MeasureTheory.lintegral_trim, MeasureTheory.lintegral_indicator, MeasureTheory.trim_measurableSet_eq, MeasureTheory.condLExp_of_not_sub_sigma_measurable, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
rw₁ rw₂ : ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
rw [setLIntegral_trim hm (measurable_condLExp _ _ _) hs, setLIntegral_condLExp _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_trim, MeasureTheory.measurable_condLExp, MeasureTheory.setLIntegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
⊢ ∫⁻ (ω : Ω), P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω), X ω ∂P

Tactic:
simpa [← setLIntegral_univ] using setLIntegral_condLExp _ _ _ .univ

Premises used: MeasureTheory.setLIntegral_condLExp, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 < ∞
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 < ∞

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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞

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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ AEMeasurable P⁻[f|mΩ] P

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
rwa rwa₁ rwa₂ rwa₃ : ∫⁻ (ω : Ω), f ω ∂P ≠ ∞
⊢ ∫⁻ (x : Ω), P⁻[f|mΩ] x ∂P ≠ ∞

Tactic:
rwa [lintegral_condLExp]

Premises used: MeasureTheory.lintegral_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞

Tactic:
exact ae_lt_top' (by fun_prop) (by rwa [lintegral_condLExp])

Premises used: MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x < ∞

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 Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
x : Ω
hx : P⁻[f|mΩ] x < ∞
⊢ P⁻[f|mΩ] x ≠ ∞

Tactic:
hx.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
h₁ h₂ : ∀ (x : Ω) (hx : P⁻[f|mΩ] x < ∞), P⁻[f|mΩ] x ≠ ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f|mΩ] x ≠ ∞

Tactic:
filter_upwards [condLExp_lt_top hf] with x hx using hx.ne

Premises used: MeasureTheory.condLExp_lt_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
h12 : Y =ᶠ[ae (P.trim hm)] P⁻[X|mΩ]
m : MeasurableSpace Ω
hm₁ : mΩ ≤ mΩ₀
⊢ Y =ᶠ[ae P] P⁻[X|mΩ]

Tactic:
apply ae_eq_of_ae_eq_trim

Premises used: MeasureTheory.ae_eq_of_ae_eq_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
⊢ AEMeasurable P⁻[X|mΩ] (P.trim hm)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
h12 :
  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
⊢ 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

Tactic:
_