awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ

Tactic:
integrable_const _

Premises used: MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ

Tactic:
exact integrable_const _

Premises used: MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ

Tactic:
hX.integrable_mul hY

Premises used: MeasureTheory.MemLp.integrable_mul
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ

Tactic:
exact hX.integrable_mul hY

Premises used: MeasureTheory.MemLp.integrable_mul
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
exact hX.mul_const _ |>.integrable (by simp)

Premises used: MeasureTheory.MemLp.integrable, MeasureTheory.MemLp.mul_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
exact (hX.integrable_mul hY).sub (hX.mul_const _ |>.integrable (by simp))

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.integrable, MeasureTheory.Integrable.sub, MeasureTheory.MemLp.mul_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ

Tactic:
exact (hY.const_mul _ |>.integrable (by simp)).sub (integrable_const _)

Premises used: MeasureTheory.MemLp.const_mul, MeasureTheory.MemLp.integrable, MeasureTheory.Integrable.sub, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
⊢ cov[0, Y; μ] = 0

Tactic:
simp [covariance]

Premises used: ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ cov[X, 0; μ] = 0

Tactic:
simp [covariance]

Premises used: ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
⊢ covariance (mΩ := mΩ) X Y 0 = 0

Tactic:
simp [covariance]

Premises used: ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
e_f :
  ∀ (x : Ω),
    (X x - ∫ (x : Ω), X x ∂μ) * (Y x - ∫ (x : Ω), Y x ∂μ) = (Y x - ∫ (x : Ω), Y x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ)
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (ω : Ω), (Y ω - ∫ (x : Ω), Y x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
x : Ω
⊢ (X x - ∫ (x : Ω), X x ∂μ) * (Y x - ∫ (x : Ω), Y x ∂μ) = (Y x - ∫ (x : Ω), Y x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ)

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
c : ℝ
⊢ cov[fun (x : Ω) ↦ c, Y; μ] = 0

Tactic:
simp [covariance]

Premises used: ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
c : ℝ
⊢ cov[X, fun (x : Ω) ↦ c; μ] = 0

Tactic:
simp [covariance]

Premises used: ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
e_f :
  ∀ (ω : Ω),
    (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) =
      (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
funProp : ‖c‖ₑ ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ c) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
e_f :
  (X ω + c - HAdd.hAdd (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), c ∂μ)) * (Y ω - ∫ (x : Ω), Y x ∂μ) =
    (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)
⊢ (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)

Tactic:
rw [integral_add hX (by fun_prop)]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
⊢ (X ω + c - HAdd.hAdd (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), c ∂μ)) * (Y ω - ∫ (x : Ω), Y x ∂μ) =
    (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
simp_rw : cov[fun (ω : Ω) ↦ X ω + c, Y; μ] = cov[X, Y; μ]
⊢ cov[fun (ω : Ω) ↦ c + X ω, Y; μ] = cov[X, Y; μ]

Tactic:
simp_rw [add_comm c]

Premises used: add_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun (ω : Ω) ↦ X ω + c, Y; μ] = cov[X, Y; μ]

Tactic:
covariance_add_const_left hX c

Premises used: ProbabilityTheory.covariance_add_const_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun (ω : Ω) ↦ X ω + c, Y; μ] = cov[X, Y; μ]

Tactic:
exact covariance_add_const_left hX c

Premises used: ProbabilityTheory.covariance_add_const_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
rw : cov[fun (ω : Ω) ↦ Y ω + c, X; μ] = cov[X, Y; μ]
rw₁ : cov[Y, X; μ] = cov[X, Y; μ]
rw₂ rw₃ : cov[X, Y; μ] = cov[X, Y; μ]
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]

Tactic:
rw [covariance_comm, covariance_add_const_left hY c, covariance_comm]

Premises used: ProbabilityTheory.covariance_add_const_left, ProbabilityTheory.covariance_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
simp_rw : cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]
⊢ cov[X, fun (ω : Ω) ↦ c + Y ω; μ] = cov[X, Y; μ]

Tactic:
simp_rw [add_comm c]

Premises used: add_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]

Tactic:
covariance_add_const_right hY c

Premises used: ProbabilityTheory.covariance_add_const_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]

Tactic:
exact covariance_add_const_right hY c

Premises used: ProbabilityTheory.covariance_add_const_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
rw :
  Eq (α := ℝ) (∫ (ω : Ω), (X ω + Y ω - ∫ (x : Ω), X x + Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ)
    (∫ (a : Ω),
      (X a - ∫ (x : Ω), X x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) + (Y a - ∫ (x : Ω), Y x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) ∂μ)
hf : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ
hg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (Y ω - ∫ (x : Ω), Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ
⊢ ∫ (ω : Ω), (X ω + Y ω - ∫ (x : Ω), X x + Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ)
      (∫ (ω : Ω), (Y ω - ∫ (x : Ω), Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ)

Tactic:
rw [← integral_add]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
e_f :
  ∀ (x : Ω),
    (X x + Y x - ∫ (x : Ω), X x + Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) =
      (X x - ∫ (x : Ω), X x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) + (Y x - ∫ (x : Ω), Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ)
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω + Y ω - ∫ (x : Ω), X x + Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ) ∂μ)
    (∫ (a : Ω),
      (X a - ∫ (x : Ω), X x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) + (Y a - ∫ (x : Ω), Y x ∂μ) * (Z a - ∫ (x : Ω), Z x ∂μ) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
x : Ω
⊢ LE.le (α := ENNReal) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
x : Ω
e_f :
  (X x + Y x - HAdd.hAdd (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), Y a ∂μ)) * (Z x - ∫ (x : Ω), Z x ∂μ) =
    (X x - ∫ (x : Ω), X x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) + (Y x - ∫ (x : Ω), Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ)
⊢ (X x + Y x - ∫ (x : Ω), X x + Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) =
    (X x - ∫ (x : Ω), X x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) + (Y x - ∫ (x : Ω), Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ)

Tactic:
rw [integral_add (hX.integrable (by simp)) (hY.integrable (by simp))]

Premises used: MeasureTheory.MemLp.integrable, MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
x : Ω
⊢ (X x + Y x - HAdd.hAdd (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), Y a ∂μ)) * (Z x - ∫ (x : Ω), Z x ∂μ) =
    (X x - ∫ (x : Ω), X x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ) + (Y x - ∫ (x : Ω), Y x ∂μ) * (Z x - ∫ (x : Ω), Z x ∂μ)

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ

Tactic:
(hX.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ

Tactic:
exact (hX.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (Y ω - ∫ (x : Ω), Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ

Tactic:
(hY.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (Y ω - ∫ (x : Ω), Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ

Tactic:
exact (hY.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
rw : cov[Y + Z, X; μ] = cov[X, Y; μ] + cov[X, Z; μ]
rw₁ : cov[Y, X; μ] + cov[Z, X; μ] = cov[X, Y; μ] + cov[X, Z; μ]
rw₂ : cov[Y, X; μ] + cov[Z, X; μ] = cov[Y, X; μ] + cov[X, Z; μ]
rw₃ rw₄ : cov[Y, X; μ] + cov[X, Z; μ] = cov[Y, X; μ] + cov[X, Z; μ]
⊢ cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]

Tactic:
rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]

Premises used: ProbabilityTheory.covariance_add_left, ProbabilityTheory.covariance_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
simp_rw :
  ∫ (ω : Ω), ((c • X) ω - ∫ (x : Ω), (c • X) x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
    c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
simp_rw₁ :
  ∫ (ω : Ω), (c • X ω - ∫ (x : Ω), c • X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
    c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
simp_rw₂ :
  ∫ (ω : Ω), (c * X ω - ∫ (x : Ω), c * X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
    c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
simp_rw₃ :
  Eq (α := ℝ) (∫ (ω : Ω), (c * X ω - ∫ (x : Ω), c * X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (a : Ω), c * ((X a - ∫ (x : Ω), X x ∂μ) * (Y a - ∫ (x : Ω), Y x ∂μ)) ∂μ)
simp_rw₄ :
  Eq (α := ℝ) (∫ (ω : Ω), (c * X ω - ∫ (x : Ω), c * X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (a : Ω), c * (X a - ∫ (x : Ω), X x ∂μ) * (Y a - ∫ (x : Ω), Y x ∂μ) ∂μ)
simp_rw₅ :
  Eq (α := ℝ)
    (∫ (ω : Ω), (c * X ω - ∫ (x : Ω), c * X x ∂μ) * Y ω - (c * X ω - ∫ (x : Ω), c * X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ)
    (∫ (a : Ω), (c * X a - c * ∫ (x : Ω), X x ∂μ) * Y a - (c * X a - c * ∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ)
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]

Tactic:
simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, mul_sub, mul_assoc, ProbabilityTheory.covariance, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
rw : cov[c • Y, X; μ] = c * cov[X, Y; μ]
rw₁ : c * cov[Y, X; μ] = c * cov[X, Y; μ]
rw₂ rw₃ : c * cov[X, Y; μ] = c * cov[X, Y; μ]
⊢ cov[X, c • Y; μ] = c * cov[X, Y; μ]

Tactic:
rw [covariance_comm, covariance_smul_left, covariance_comm]

Premises used: ProbabilityTheory.covariance_smul_left, ProbabilityTheory.covariance_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[fun (ω : Ω) ↦ c * X ω, Y; μ] = c * cov[X, Y; μ]

Tactic:
covariance_smul_left c

Premises used: ProbabilityTheory.covariance_smul_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ c * Y ω; μ] = c * cov[X, Y; μ]

Tactic:
covariance_smul_right c

Premises used: ProbabilityTheory.covariance_smul_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[fun (ω : Ω) ↦ X ω * c, Y; μ] = cov[X, Y; μ] * c

Tactic:
simp [mul_comm, covariance_const_mul_left]

Premises used: mul_comm, ProbabilityTheory.covariance_const_mul_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω * c; μ] = cov[X, Y; μ] * c

Tactic:
simp [mul_comm, covariance_const_mul_right]

Premises used: ProbabilityTheory.covariance_const_mul_right, mul_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
simp_rw : cov[fun (ω : Ω) ↦ c⁻¹ * X ω, Y; μ] = c⁻¹ * cov[X, Y; μ]
⊢ cov[fun (ω : Ω) ↦ X ω / c, Y; μ] = cov[X, Y; μ] / c

Tactic:
simp_rw [← inv_mul_eq_div, covariance_const_mul_left]

Premises used: inv_mul_eq_div, ProbabilityTheory.covariance_const_mul_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
simp_rw : cov[X, fun (ω : Ω) ↦ c⁻¹ * Y ω; μ] = c⁻¹ * cov[X, Y; μ]
⊢ cov[X, fun (ω : Ω) ↦ Y ω / c; μ] = cov[X, Y; μ] / c

Tactic:
simp_rw [← inv_mul_eq_div, covariance_const_mul_right]

Premises used: inv_mul_eq_div, ProbabilityTheory.covariance_const_mul_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[-X, Y; μ] = cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
rw : -1 * cov[X, Y; μ] = -cov[X, Y; μ]
⊢ cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ] = -cov[X, Y; μ]

Tactic:
rw [covariance_smul_left]

Premises used: ProbabilityTheory.covariance_smul_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ -1 * cov[X, Y; μ] = -cov[X, Y; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
calc : cov[-X, Y; μ] = cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ]
calc₁ : cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ] = -cov[X, Y; μ]
⊢ cov[-X, Y; μ] = -cov[X, Y; μ]

Tactic:
calc cov[-X, Y; μ]
  _ = cov[(-1 : ℝ) • X, Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_left]; simp

Premises used: OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[fun (ω : Ω) ↦ -X ω, Y; μ] = -cov[X, Y; μ]

Tactic:
covariance_neg_left

Premises used: ProbabilityTheory.covariance_neg_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, -Y; μ] = cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
rw : -1 * cov[X, Y; μ] = -cov[X, Y; μ]
⊢ cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ] = -cov[X, Y; μ]

Tactic:
rw [covariance_smul_right]

Premises used: ProbabilityTheory.covariance_smul_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
calc : cov[X, -Y; μ] = cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ]
calc₁ : cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ] = -cov[X, Y; μ]
⊢ cov[X, -Y; μ] = -cov[X, Y; μ]

Tactic:
calc cov[X, -Y; μ]
  _ = cov[X, (-1 : ℝ) • Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_right]; simp

Premises used: OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, fun (ω : Ω) ↦ -Y ω; μ] = -cov[X, Y; μ]

Tactic:
covariance_neg_right

Premises used: ProbabilityTheory.covariance_neg_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
simp_rw : cov[X + -Y, Z; μ] = cov[X, Z; μ] + -cov[Y, Z; μ]
simp_rw₁ : cov[X, Z; μ] + cov[-Y, Z; μ] = cov[X, Z; μ] + -cov[Y, Z; μ]
⊢ cov[X - Y, Z; μ] = cov[X, Z; μ] - cov[Y, Z; μ]

Tactic:
simp_rw [sub_eq_add_neg, covariance_add_left hX hY.neg hZ, covariance_neg_left]

Premises used: ProbabilityTheory.covariance_neg_left, ProbabilityTheory.covariance_add_left, sub_eq_add_neg, MeasureTheory.MemLp.neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[fun (ω : Ω) ↦ X ω - Y ω, Z; μ] = cov[X, Z; μ] - cov[Y, Z; μ]

Tactic:
covariance_sub_left hX hY hZ

Premises used: ProbabilityTheory.covariance_sub_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
simp_rw : cov[X, Y + -Z; μ] = cov[X, Y; μ] + -cov[X, Z; μ]
simp_rw₁ : cov[X, Y; μ] + cov[X, -Z; μ] = cov[X, Y; μ] + -cov[X, Z; μ]
⊢ cov[X, Y - Z; μ] = cov[X, Y; μ] - cov[X, Z; μ]

Tactic:
simp_rw [sub_eq_add_neg, covariance_add_right hX hY hZ.neg, covariance_neg_right]

Premises used: sub_eq_add_neg, ProbabilityTheory.covariance_neg_right, ProbabilityTheory.covariance_add_right, MeasureTheory.MemLp.neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X, fun (ω : Ω) ↦ Y ω - Z ω; μ] = cov[X, Y; μ] - cov[X, Z; μ]

Tactic:
covariance_sub_right hX hY hZ

Premises used: ProbabilityTheory.covariance_sub_right
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun (ω : Ω) ↦ X ω - c, Y; μ] = cov[X, Y; μ]

Tactic:
simp [sub_eq_add_neg, hX]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun (ω : Ω) ↦ c - X ω, Y; μ] = -cov[X, Y; μ]

Tactic:
simp [sub_eq_add_neg, hX.fun_neg]

Premises used: MeasureTheory.Integrable.fun_neg, sub_eq_add_neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω - c; μ] = cov[X, Y; μ]

Tactic:
simp [sub_eq_add_neg, hY]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ c - Y ω; μ] = -cov[X, Y; μ]

Tactic:
simp [sub_eq_add_neg, hY.fun_neg]

Premises used: MeasureTheory.Integrable.fun_neg, sub_eq_add_neg
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
hX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (X i) 2 μ
⊢ cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, cov[X i, Y; μ]

Tactic:
simp