awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
hf₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
hf₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
hg₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
hf₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
hg₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
hf₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg₂ : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have simp_rw : ∫ (a : Ω), X a * Y a ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
    (HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
      HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)) =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: simp_rw [integral_mul_const, integral_const_mul, integral_const, probReal_univ,
       one_smul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (ω : Ω), (Y ω - ∫ (x : Ω), Y x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)
have e_f : ∀ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) * (Y x - ∫ (x : Ω), Y x ∂μ) = (Y x - ∫ (x : Ω), Y x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
    (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ)
have e_f : ∀ (ω : Ω),
  (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ c) μ
have funProp : ‖c‖ₑ ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
⊢ (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)
have e_f : (X ω + c - HAdd.hAdd (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), c ∂μ)) * (Y ω - ∫ (x : Ω), Y x ∂μ) =
  (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)
Tactic: rw [integral_add hX (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun (ω : Ω) ↦ c + X ω, Y; μ] = cov[X, Y; μ]
have simp_rw : cov[fun (ω : Ω) ↦ X ω + c, Y; μ] = cov[X, Y; μ]
Tactic: simp_rw [add_comm c]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]
have rw : cov[fun (ω : Ω) ↦ Y ω + c, X; μ] = cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_add_const_left hY c, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
rw : cov[fun (ω : Ω) ↦ Y ω + c, X; μ] = cov[X, Y; μ]
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]
have rw₁ : cov[Y, X; μ] = cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_add_const_left hY c, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]
have rw₂ : cov[X, Y; μ] = cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_add_const_left hY c, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ c + Y ω; μ] = cov[X, Y; μ]
have simp_rw : cov[X, fun (ω : Ω) ↦ Y ω + c; μ] = cov[X, Y; μ]
Tactic: simp_rw [add_comm c]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ω + 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 ∂μ) ∂μ)
have 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 ∂μ) ∂μ)
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ)
⊢ ∫ (ω : Ω), (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 ∂μ) ∂μ)
have hf : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ)) μ
⊢ ∫ (ω : Ω), (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 ∂μ) ∂μ)
have hg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (Y ω - ∫ (x : Ω), Y x ∂μ) * (Z ω - ∫ (x : Ω), Z x ∂μ)) μ
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ 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 ∂μ) ∂μ)
have 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 ∂μ)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 - ∫ (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 ∂μ)
have 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 ∂μ)
Tactic: rw [integral_add (hX.integrable (by simp)) (hY.integrable (by simp))]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]
have rw : cov[Y + Z, X; μ] = cov[X, Y; μ] + cov[X, Z; μ]
Tactic: rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]
have rw₁ : cov[Y, X; μ] + cov[Z, X; μ] = cov[X, Y; μ] + cov[X, Z; μ]
Tactic: rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]
have rw₂ : cov[Y, X; μ] + cov[Z, X; μ] = cov[Y, X; μ] + cov[X, Z; μ]
Tactic: rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]
have rw₃ : cov[Y, X; μ] + cov[X, Z; μ] = cov[Y, X; μ] + cov[X, Z; μ]
Tactic: rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have simp_rw : ∫ (ω : Ω), ((c • X) ω - ∫ (x : Ω), (c • X) x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
  c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have simp_rw₁ : ∫ (ω : Ω), (c • X ω - ∫ (x : Ω), c • X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
  c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have simp_rw₂ : ∫ (ω : Ω), (c * X ω - ∫ (x : Ω), c * X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
  c * ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have 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 ∂μ)) ∂μ)
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ)) ∂μ)
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have 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 ∂μ) ∂μ)
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ)
⊢ cov[c • X, Y; μ] = c * cov[X, Y; μ]
have 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 ∂μ ∂μ)
Tactic: simp_rw [covariance, Pi.smul_apply, smul_eq_mul, ← integral_const_mul, ← mul_assoc, mul_sub,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[X, c • Y; μ] = c * cov[X, Y; μ]
have rw : cov[c • Y, X; μ] = c * cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_smul_left, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
rw : cov[c • Y, X; μ] = c * cov[X, Y; μ]
⊢ cov[X, c • Y; μ] = c * cov[X, Y; μ]
have rw₁ : c * cov[Y, X; μ] = c * cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_smul_left, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[X, c • Y; μ] = c * cov[X, Y; μ]
have rw₂ : c * cov[X, Y; μ] = c * cov[X, Y; μ]
Tactic: rw [covariance_comm, covariance_smul_left, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[fun (ω : Ω) ↦ X ω / c, Y; μ] = cov[X, Y; μ] / c
have simp_rw : cov[fun (ω : Ω) ↦ c⁻¹ * X ω, Y; μ] = c⁻¹ * cov[X, Y; μ]
Tactic: simp_rw [← inv_mul_eq_div, covariance_const_mul_left]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[X, fun (ω : Ω) ↦ Y ω / c; μ] = cov[X, Y; μ] / c
have simp_rw : cov[X, fun (ω : Ω) ↦ c⁻¹ * Y ω; μ] = c⁻¹ * cov[X, Y; μ]
Tactic: simp_rw [← inv_mul_eq_div, covariance_const_mul_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ] = -cov[X, Y; μ]
have rw : -1 * cov[X, Y; μ] = -cov[X, Y; μ]
Tactic: rw [covariance_smul_left]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[-X, Y; μ] = -cov[X, Y; μ]
have calc : cov[-X, Y; μ] = cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ]
Tactic: calc cov[-X, Y; μ]
  _ = cov[(-1 : ℝ) • X, Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_left]; simp
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
calc : cov[-X, Y; μ] = cov[HSMul.hSMul (α := ℝ) (-1) X, Y; μ]
⊢ cov[-X, Y; μ] = -cov[X, Y; μ]
have calc₁ : cov[HSMul.hSMul (α := ℝ) (-1) 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
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ] = -cov[X, Y; μ]
have rw : -1 * cov[X, Y; μ] = -cov[X, Y; μ]
Tactic: rw [covariance_smul_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, -Y; μ] = -cov[X, Y; μ]
have calc : cov[X, -Y; μ] = cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ]
Tactic: calc cov[X, -Y; μ]
  _ = cov[X, (-1 : ℝ) • Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_right]; simp
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
calc : cov[X, -Y; μ] = cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ]
⊢ cov[X, -Y; μ] = -cov[X, Y; μ]
have calc₁ : cov[X, HSMul.hSMul (α := ℝ) (-1) Y; μ] = -cov[X, Y; μ]
Tactic: calc cov[X, -Y; μ]
  _ = cov[X, (-1 : ℝ) • Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_right]; simp
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 - Y, Z; μ] = cov[X, Z; μ] - cov[Y, Z; μ]
have simp_rw : 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]