awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
ω : Ω
hω : μ[c • X | m] ω = (c • μ[X | m]) ω
⊢ HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 ω = (HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2) ω

Tactic:
simp [hω, ← mul_sub, mul_pow]

Premises used: mul_sub, mul_pow
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • Var[X; μ | m]

Tactic:
condExp_smul ..

Premises used: MeasureTheory.condExp_smul, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
μ₁ : Var[c • X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m]
⊢ Var[c • X; μ | m] =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • Var[X; μ | m]

Tactic:
calc
    Var[c • X; μ | m]
    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]
    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..

Premises used: HSub.hSub, MeasureTheory.condExp_smul, MeasureTheory.condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ Var[-X; μ | m] =ᶠ[ae μ] Var[X; μ | m]

Tactic:
condExp_congr_ae ?_

Premises used: MeasureTheory.condExp_congr_ae, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
refine : HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (X - μ[X | m]) 2
⊢ Var[-X; μ | m] =ᶠ[ae μ] Var[X; μ | m]

Tactic:
refine condExp_congr_ae ?_

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
h :
  ∀ (ω : Ω) (hω : μ[-X | m] ω = (-μ[X | m]) ω),
    HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 ω = HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω
⊢ HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (X - μ[X | m]) 2

Tactic:
filter_upwards [condExp_neg (m := m) X] with ω hω

Premises used: MeasureTheory.condExp_neg
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : μ[-X | m] ω = (-μ[X | m]) ω
h : HPow.hPow (β := ℕ) (-X ω + μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2
⊢ HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 ω = HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : μ[-X | m] ω = (-μ[X | m]) ω
⊢ HPow.hPow (β := ℕ) (-X ω + μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2

Tactic:
ring
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
pos : ∀ (hfint : Integrable f μ), μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
neg : ∀ (hfint : ¬Integrable f μ), μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : ¬Integrable f μ
neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ

Tactic:
rw [condExp_of_not_integrable hfint, integral_undef hfint]

Premises used: MeasureTheory.integral_undef, MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : ¬Integrable f μ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ

Tactic:
(ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint
    (fun s _ hs ↦ integrableOn_const hs.ne) (fun s hms hs => ?_)
      stronglyMeasurable_const.aestronglyMeasurable).symm

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.integrableOn_const, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm, LT.lt.ne
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
pos :
  ∀ (s : Set Ω) (hms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ) (∫ (x : Ω) in s, f x ∂μ)
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint
    (fun s _ hs ↦ integrableOn_const hs.ne) (fun s hms hs => ?_)
      stronglyMeasurable_const.aestronglyMeasurable).symm

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.integrableOn_const, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm, LT.lt.ne
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ) (∫ (x : Ω) in s, f x ∂μ)

Tactic:
rw [setIntegral_const]

Premises used: MeasureTheory.setIntegral_const
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (hfint : MemLp f 1 μ) (s : Set Ω) (hms : MeasurableSet s)
    (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ

Tactic:
rw [← memLp_one_iff_integrable] at hfint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ

Tactic:
MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_

Premises used: MeasureTheory.Measure.real, MeasureTheory.MemLp.induction_stronglyMeasurable, MeasureTheory.Measure.restrict, MeasureTheory.integral, HSMul.hSMul, Eq
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : AEStronglyMeasurable f μ
pos₁ :
  ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), s_1.indicator (fun (x : Ω) ↦ c) x ∂μ) =
          ∫ (x : Ω) in s, s_1.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ :
  ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ →
                  HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (f + g) x ∂μ) = ∫ (x : Ω) in s, (f + g) x ∂μ
pos₃ :
  IsClosed (X := ↥(lpMeas E ℝ m₁ 1 μ))
    {f : ↥(lpMeas E ℝ m₁ 1 μ) |
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ) =
        ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ}
pos₄ :
  ∀ ⦃f g : Ω → E⦄,
    f =ᶠ[ae μ] g →
      MemLp f 1 μ →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
          HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ

Tactic:
refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable f μ

Tactic:
⟨f, hf, EventuallyEq.rfl⟩

Premises used: And.intro, Exists.intro, Filter.EventuallyEq.rfl, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable f μ

Tactic:
exact ⟨f, hf, EventuallyEq.rfl⟩
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
pos :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
      ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
      ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ

Tactic:
_
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀
    (hindp :
      ∀ (t1 t2 : Set Ω),
        MeasurableSet t1 →
          MeasurableSet t2 →
            (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞))
    (hfint : MemLp f 1 μ) (s : Set Ω) (hms : MeasurableSet s)
    (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (c : E) ⦃t : Set Ω⦄ (hmt : MeasurableSet t),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
        ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ

Tactic:
rw [Indep_iff] at hindp

Premises used: ProbabilityTheory.Indep_iff
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₄ :
  (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₅ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₆ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₇ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₈ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s ∩ t, c ∂μ
pos₉ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = μ.real (s ∩ t) • c
pos₁₀ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) • c = μ.real (s ∩ t) • c
pos₁₁ pos₁₂ :
  ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) • c = ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) • c
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ

Tactic:
rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]

Premises used: MeasureTheory.integral_indicator, smul_smul, MeasureTheory.setIntegral_indicator, Set.inter_comm, ENNReal.toReal_mul, mul_comm, MeasureTheory.measureReal_def, MeasureTheory.setIntegral_const
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
pos :
  Disjoint (Function.support u) (Function.support v) →
    MemLp u 1 μ →
      MemLp v 1 μ →
        StronglyMeasurable u →
          StronglyMeasurable v →
            HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
⊢ Disjoint (Function.support u) (Function.support v) →
    MemLp u 1 μ →
      MemLp v 1 μ →
        StronglyMeasurable u →
          StronglyMeasurable v →
            HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ

Tactic:
_
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
⊢ Integrable u μ

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
⊢ Integrable v μ

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
hvint₁ : Integrable v μ
⊢ StronglyMeasurable u

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
hvint₁ : Integrable v μ
hu₁ : StronglyMeasurable u
⊢ StronglyMeasurable v

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
hvint₁ : Integrable v μ
hu₁ : StronglyMeasurable u
hv₁ : StronglyMeasurable v
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
hvint₁ : Integrable v μ
hu₁ : StronglyMeasurable u
hv₁ : StronglyMeasurable v
hu_eq₁ : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ

Tactic:
rw [memLp_one_iff_integrable] at huint hvint

Premises used: MeasureTheory.memLp_one_iff_integrable