awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h12 : ∫⁻ (x : Ω) in s, Y x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ ∫⁻ (x : Ω) in s, Y x ∂P.trim hm = ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm

Tactic:
rw [setLIntegral_trim_ae hm hY hs, setLIntegral_condLExp_trim _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_trim_ae, MeasureTheory.setLIntegral_condLExp_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
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, Y x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
hXY s hs
-- 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
h : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : Ω) in s, Y x ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
exact hXY s hs
-- 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 : Measurable Y
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ Y =ᶠ[ae P] P⁻[X|mΩ]

Tactic:
ae_eq_condLExp₀ _ _ hY.aemeasurable hXY

Premises used: Measurable.aemeasurable, MeasureTheory.ae_eq_condLExp₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
c : ℝ≥0∞
⊢ P⁻[fun (x : Ω) ↦ c|mΩ] = fun (x : Ω) ↦ c

Tactic:
condLExp_eq_self _ _ (measurable_const)

Premises used: MeasureTheory.condLExp_eq_self, measurable_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] =ᶠ[ae P] 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∞
hXY : X =ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] =ᶠ[ae P] 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∞
hXY : X =ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]

Tactic:
ae_eq_condLExp _ _ _ (measurable_condLExp _ _ _) (fun s hs ↦ ?_)

Premises used: MeasureTheory.ae_eq_condLExp, MeasureTheory.measurable_condLExp
-- 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)
pos : ∀ (s : Set Ω) (hs : MeasurableSet s), ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
⊢ P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]

Tactic:
refine ae_eq_condLExp _ _ _ (measurable_condLExp _ _ _) (fun s hs ↦ ?_)

Premises used: MeasureTheory.ae_eq_condLExp, MeasureTheory.measurable_condLExp
-- 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
pos : ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P
⊢ ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P

Tactic:
rw [setLIntegral_condLExp _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp
-- 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
pos : ∀ᵐ (x : Ω) ∂P, x ∈ s → X x = Y x
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P = ∫⁻ (ω : Ω) in s, Y ω ∂P

Tactic:
apply setLIntegral_congr_fun_ae (hm s hs)

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- 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
a : Ω
h : X a = Y a
h₁ : a ∈ s → X a = Y a
⊢ a ∈ s → X a = Y a

Tactic:
_
-- 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
a : Ω
h : X a = Y a
h_1 : a ∈ s
⊢ X a = Y a

Tactic:
h
-- 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 :
  ∀ (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₁ h₂ : ∀ (a : Ω) (h : X a = Y a), a ∈ s → X a = Y a
⊢ ∀ᵐ (x : Ω) ∂P, x ∈ s → X x = Y x

Tactic:
filter_upwards [hXY] with _ h _ using h
-- 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)
⊢ P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|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 Y : Ω → ℝ≥0∞
hXY : X =ᶠ[ae P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|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 Ω
pos : ∀ (hm : mΩ ≤ mΩ₀), P⁻[0|mΩ] = 0
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[0|mΩ] = 0
⊢ P⁻[0|mΩ] = 0

Tactic:
by_cases hm : mΩ ≤ mΩ₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[0|mΩ] = 0

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 Ω
hm : mΩ ≤ mΩ₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[0|mΩ] = 0
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[0|mΩ] = 0
⊢ P⁻[0|mΩ] = 0

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 Ω
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[0|mΩ] = 0

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 Ω
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[0|mΩ] = 0

Tactic:
condLExp_const hm P 0

Premises used: MeasureTheory.condLExp_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[0|mΩ] = 0

Tactic:
exact condLExp_const hm P 0

Premises used: MeasureTheory.condLExp_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[1|mΩ] = 1

Tactic:
condLExp_const hm P 1

Premises used: MeasureTheory.condLExp_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᶠ[ae P] Y
apply : P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] =ᶠ[ae (P.trim hm)] P⁻[Y|mΩ]

Tactic:
apply ae_eq_trim_of_measurable hm (measurable_condLExp _ _ X) (measurable_condLExp _ _ Y)

Premises used: MeasureTheory.measurable_condLExp, ae_eq_trim_of_measurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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] P⁻[Y|mΩ]

Tactic:
condLExp_congr_ae hXY

Premises used: MeasureTheory.condLExp_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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] P⁻[Y|mΩ]

Tactic:
exact condLExp_congr_ae hXY

Premises used: MeasureTheory.condLExp_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
neg :
  ∀ (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)

Tactic:
by_cases hP : IsFiniteMeasure P

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP rwa rwa₁ rwa₂ rwa₃ : ¬IsFiniteMeasure P
⊢ ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)

Tactic:
rwa [sigmaFinite_trim_bot_iff]

Premises used: MeasureTheory.sigmaFinite_trim_bot_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
⊢ ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)

Tactic:
have hσ : ¬SigmaFinite (P.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
hσ : ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)
⊢ Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [not_isFiniteMeasure_iff] at hP

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
hσ : ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)
hP₁ : Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬SigmaFinite (m0 := ⊥) (P.trim ⋯)

Tactic:
rw [not_isFiniteMeasure_iff] at hP

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 ⋯)
neg :
  Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) 0 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)

Tactic:
rw [condLExp_of_not_sigmaFinite bot_le hσ]

Premises used: MeasureTheory.condLExp_of_not_sigmaFinite, bot_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 ⋯)
⊢ Eq.{u_1 + 1} (α := Ω → ℝ≥0∞) 0 fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)

Tactic:
simp [hP, Pi.zero_def]

Premises used: Pi.zero_def
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : NeZero P
X : Ω → ℝ≥0∞
hP : IsFiniteMeasure P
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)
⊢ 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)

Premises used: Bot.bot, eq_const_of_measurable_bot, MeasureTheory.measurable_condLExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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
pos : ∀ (x : Ω), P⁻[X|⊥] 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)

Tactic:
ext _
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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 : Ω
pos : P⁻[X|⊥] x = HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), P⁻[X|⊥] ω ∂P)
⊢ P⁻[X|⊥] x = HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)

Tactic:
rw [← lintegral_condLExp bot_le]

Premises used: MeasureTheory.lintegral_condLExp, bot_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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∞) (∫⁻ (ω : Ω), P⁻[X|⊥] ω ∂P)

Tactic:
simp [h_eq, mul_comm, mul_assoc, ENNReal.mul_inv_cancel
    (NeZero.ne (P .univ)) (measure_ne_top _ _)]

Premises used: Set.univ, mul_assoc, MeasureTheory.measure_ne_top, ENNReal.mul_inv_cancel, mul_comm, DFunLike.coe, NeZero.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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)
inr :
  ∀ (hP : NeZero P),
    P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
      HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂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

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
inl :
  condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[⊥] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), 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)

Tactic:
rw [ae_zero]

Premises used: MeasureTheory.ae_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
⊢ condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[⊥] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)

Tactic:
Filter.eventually_bot

Premises used: Filter.EventuallyEq, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
X : Ω → ℝ≥0∞
⊢ condLExp (mΩ₀ := mΩ₀) ⊥ 0 X =ᶠ[⊥] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((0 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂0)

Tactic:
exact Filter.eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hP : NeZero P
⊢ P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)

Tactic:
ae_of_all P <| congr_fun (condLExp_bot' P X)

Premises used: MeasureTheory.condLExp_bot', Filter.EventuallyEq, MeasureTheory.ae_of_all, congr_fun
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hP : NeZero P
⊢ P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) ↦
    HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P)

Tactic:
exact ae_of_all P <| congr_fun (condLExp_bot' P X)

Premises used: MeasureTheory.condLExp_bot', MeasureTheory.ae_of_all, congr_fun
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
Goal:
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ≥0∞
⊢ Eq.{u_1 + 1} (α := Ω → ℝ≥0∞)
    (fun (x : Ω) ↦ HSMul.hSMul (α := ℝ≥0∞) (((P : (a : Set Ω) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∫⁻ (ω : Ω), X ω ∂P))
    fun (x : Ω) ↦ ∫⁻ (ω : Ω), X ω ∂P

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation
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Ω]
neg : ∀ (hm : ¬mΩ ≤ mΩ₀), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] 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∞
hXY : X ≤ᶠ[ae P] Y
hm : ¬mΩ ≤ mΩ₀
neg : (ae P).EventuallyLE (β := ℝ≥0∞) 0 0
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_le hm, Filter.EventuallyLE.rfl]

Premises used: Filter.EventuallyLE.rfl, MeasureTheory.condLExp_of_not_le
-- 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Ω₀
pos : ∀ (hσ : SigmaFinite (P.trim hm)), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
neg : ∀ (hσ : ¬SigmaFinite (P.trim hm)), P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] 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∞
hXY : X ≤ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
neg : (ae P).EventuallyLE (β := ℝ≥0∞) 0 0
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ, Filter.EventuallyLE.rfl]

Premises used: Filter.EventuallyLE.rfl, MeasureTheory.condLExp_of_not_sigmaFinite
-- 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)
pos : P⁻[X|mΩ] ≤ᶠ[ae (P.trim hm)] P⁻[Y|mΩ]
pos₁ : MeasurableSpace Ω
pos₂ : mΩ ≤ mΩ₀
⊢ P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[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∞
hXY : X ≤ᶠ[ae P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable P⁻[X|mΩ]

Tactic:
fun_prop
-- 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
pos :
  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
⊢ 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

Tactic:
_
-- 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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[Y|mΩ] x ∂P.trim hm
⊢ ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[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∞
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∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (x : Ω) in s, P⁻[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∞
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∞)
pos : ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P
⊢ ∫⁻ (x : Ω) in s, P⁻[X|mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[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∞
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∞)
pos : ∀ᵐ (x : Ω) ∂P, x ∈ s → X x ≤ Y x
⊢ ∫⁻ (ω : Ω) in s, X ω ∂P ≤ ∫⁻ (ω : Ω) in s, Y ω ∂P

Tactic:
apply setLIntegral_mono_ae' (hm s hs)

Premises used: MeasureTheory.setLIntegral_mono_ae'
-- 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 : LT.lt (α := ℝ≥0∞) ((P.trim hm : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (a : Ω), X a ≤ Y a → a ∈ s → X a ≤ Y a

Tactic:
fun _ h _ ↦ h