awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ Insert.insert i s, MemLp (X i_1) 2 μ
insert : ∀ i ∈ s, MemLp (X i) 2 μ
insert₁ : MemLp (X i) 2 μ
insert₂ : MemLp (ε := ℝ) (∑ x ∈ s, X x) 2 μ
insert₃ : MemLp Y 2 μ
⊢ cov[∑ i ∈ Insert.insert i s, X i, Y; μ] = ∑ i ∈ Insert.insert i s, cov[X i, Y; μ]

Tactic:
rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]

Premises used: ProbabilityTheory.covariance_add_left, Finset.sum_insert
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
j : ι
hj : j ∈ s
⊢ j ∈ insert i s

Tactic:
simp [hj]
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ ∀ i ∈ s, MemLp (X i) 2 μ

Tactic:
exact fun j hj ↦ hX j (by simp [hj])
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ i ∈ insert i s

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (X i) 2 μ

Tactic:
exact hX i (by simp)
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (ε := ℝ) (∑ x ∈ s, X x) 2 μ

Tactic:
exact memLp_finsetSum' s (fun j hj ↦ hX j (by simp [hj]))

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
hY
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s_1 : Finset ι
inst : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
exact hY
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
empty :
  ∀ (hX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (X i) 2 μ),
    cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, cov[X i, Y; μ]
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ])
    (hX : ∀ i_1 ∈ Insert.insert i s, MemLp (X i_1) 2 μ),
    cov[∑ i ∈ Insert.insert i s, X i, Y; μ] = ∑ i ∈ Insert.insert i s, cov[X i, Y; μ]
⊢ cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert i s hi h_ind =>
    rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
    · exact fun j hj ↦ hX j (by simp [hj])
    · exact hX i (by simp)
    · exact memLp_finsetSum' s (fun j hj ↦ hX j (by simp [hj]))
    · exact hY

Premises used: ProbabilityTheory.covariance_add_left, MeasureTheory.memLp_finsetSum', Insert.insert
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
empty :
  ∀ (hX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (X i) 2 μ),
    cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, cov[X i, Y; μ]
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (h_ind : ∀ (hX : ∀ i ∈ s, MemLp (X i) 2 μ), cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ])
    (hX : ∀ i_1 ∈ Insert.insert i s, MemLp (X i_1) 2 μ),
    cov[∑ i ∈ Insert.insert i s, X i, Y; μ] = ∑ i ∈ Insert.insert i s, cov[X i, Y; μ]
⊢ cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi h_ind =>
    rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
    · exact fun j hj ↦ hX j (by simp [hj])
    · exact hX i (by simp)
    · exact memLp_finsetSum' s (fun j hj ↦ hX j (by simp [hj]))
    · exact hY

Premises used: ProbabilityTheory.covariance_add_left, MeasureTheory.memLp_finsetSum', Insert.insert
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ cov[∑ i : ι, X i, Y; μ] = ∑ i : ι, cov[X i, Y; μ]

Tactic:
covariance_sum_left' (fun _ _ ↦ hX _) hY

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

Tactic:
covariance_sum_left' hX hY

Premises used: ProbabilityTheory.covariance_sum_left'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
⊢ cov[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]

Tactic:
convert! covariance_sum_left' hX hY

Premises used: ProbabilityTheory.covariance_sum_left'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ cov[∑ i : ι, X i, Y; μ] = ∑ i : ι, cov[X i, Y; μ]

Tactic:
covariance_sum_left hX hY

Premises used: ProbabilityTheory.covariance_sum_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
⊢ cov[fun (ω : Ω) ↦ ∑ i : ι, X i ω, Y; μ] = ∑ i : ι, cov[X i, Y; μ]

Tactic:
convert! covariance_sum_left hX hY

Premises used: ProbabilityTheory.covariance_sum_left
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, Y; μ]) (∑ i ∈ s, cov[Y, X i; μ])
⊢ cov[Y, ∑ i ∈ s, X i; μ] = ∑ i ∈ s, cov[Y, X i; μ]

Tactic:
rw [covariance_comm, covariance_sum_left' hX hY]

Premises used: ProbabilityTheory.covariance_sum_left', ProbabilityTheory.covariance_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ Eq (α := ℝ) (∑ i ∈ s, cov[X i, Y; μ]) (∑ i ∈ s, cov[Y, X i; μ])

Tactic:
simp_rw [covariance_comm]

Premises used: ProbabilityTheory.covariance_comm
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ cov[Y, ∑ i : ι, X i; μ] = ∑ i : ι, cov[Y, X i; μ]

Tactic:
covariance_sum_right' (fun _ _ ↦ hX _) hY

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

Tactic:
covariance_sum_right' hX hY

Premises used: ProbabilityTheory.covariance_sum_right'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
⊢ cov[Y, fun (ω : Ω) ↦ ∑ i ∈ s, X i ω; μ] = ∑ i ∈ s, cov[Y, X i; μ]

Tactic:
convert! covariance_sum_right' hX hY

Premises used: ProbabilityTheory.covariance_sum_right'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ cov[Y, fun (ω : Ω) ↦ ∑ i : ι, X i ω; μ] = ∑ i : ι, cov[Y, X i; μ]

Tactic:
covariance_fun_sum_right' (fun _ _ ↦ hX _) hY

Premises used: ProbabilityTheory.covariance_fun_sum_right'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ]) (∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ])
rw₁ : MemLp (ε := ℝ) (∑ j ∈ t, Y j) 2 μ
⊢ cov[∑ i ∈ s, X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
rw [covariance_sum_left' hX]

Premises used: ProbabilityTheory.covariance_sum_left'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
i : ι
hi : i ∈ s
rw rw₁ : Eq (α := ℝ) (∑ i_1 ∈ t, cov[X i, Y i_1; μ]) (∑ j ∈ t, cov[X i, Y j; μ])
⊢ cov[X i, ∑ j ∈ t, Y j; μ] = ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
rw [covariance_sum_right' hY (hX i hi)]

Premises used: ProbabilityTheory.covariance_sum_right'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ]) (∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ])

Tactic:
exact Finset.sum_congr rfl fun i hi ↦ by rw [covariance_sum_right' hY (hX i hi)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (ε := ℝ) (∑ j ∈ t, Y j) 2 μ

Tactic:
memLp_finsetSum' t hY

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (ε := ℝ) (∑ j ∈ t, Y j) 2 μ

Tactic:
exact memLp_finsetSum' t hY

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
ι' : Type u_3
inst_2 : Fintype ι'
Y : ι' → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : ∀ (i : ι'), MemLp (Y i) 2 μ
⊢ cov[∑ i : ι, X i, ∑ j : ι', Y j; μ] = ∑ i : ι, ∑ j : ι', cov[X i, Y j; μ]

Tactic:
covariance_sum_sum' (fun _ _ ↦ hX _) (fun _ _ ↦ hY _)

Premises used: ProbabilityTheory.covariance_sum_sum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ cov[∑ i ∈ s, X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
covariance_sum_sum' hX hY

Premises used: ProbabilityTheory.covariance_sum_sum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
h₁ : ∀ (x : Ω), Eq (α := ℝ) (∑ j ∈ t, Y j x) ((∑ j ∈ t, Y j) x)
⊢ cov[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω, fun (ω : Ω) ↦ ∑ j ∈ t, Y j ω; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
convert! covariance_sum_sum' hX hY

Premises used: ProbabilityTheory.covariance_sum_sum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ j ∈ t, Y j x) ((∑ j ∈ t, Y j) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
ι' : Type u_3
inst_2 : Fintype ι'
Y : ι' → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : ∀ (i : ι'), MemLp (Y i) 2 μ
⊢ cov[fun (ω : Ω) ↦ ∑ i : ι, X i ω, fun (ω : Ω) ↦ ∑ j : ι', Y j ω; μ] = ∑ i : ι, ∑ j : ι', cov[X i, Y j; μ]

Tactic:
covariance_fun_sum_fun_sum' (fun _ _ ↦ hX _) (fun _ _ ↦ hY _)

Premises used: ProbabilityTheory.covariance_fun_sum_fun_sum'
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.map (⇑Z : (a : Ω') → Ω) μ) fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map (⇑Z : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map (⇑Z : (a : Ω') → Ω) μ) fun (x : Ω) ↦ Y x))
    (∫ (ω : Ω'),
      ((X ∘ (⇑Z : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Z : (a : Ω') → Ω)) x ∂μ) *
        ((Y ∘ (⇑Z : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (Y ∘ (⇑Z : (a : Ω') → Ω)) x ∂μ) ∂μ)
simp_rw₁ :
  Eq (α := ℝ)
    (∫ (x : Ω'),
      (X ((Z : (a : Ω') → Ω) x) - ∫ (x : Ω'), X ((Z : (a : Ω') → Ω) x) ∂μ) *
        (Y ((Z : (a : Ω') → Ω) x) - ∫ (x : Ω'), Y ((Z : (a : Ω') → Ω) x) ∂μ) ∂μ)
    (∫ (ω : Ω'),
      ((X ∘ (⇑Z : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Z : (a : Ω') → Ω)) x ∂μ) *
        ((Y ∘ (⇑Z : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (Y ∘ (⇑Z : (a : Ω') → Ω)) x ∂μ) ∂μ)
⊢ covariance (mΩ := mΩ) X Y (Measure.map (⇑Z : (a : Ω') → Ω) μ) =
    cov[X ∘ (⇑Z : (a : Ω') → Ω), Y ∘ (⇑Z : (a : Ω') → Ω); μ]

Tactic:
simp_rw [covariance, integral_map_equiv, Function.comp_apply]

Premises used: MeasureTheory.integral_map_equiv, ProbabilityTheory.covariance, Function.comp_apply
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.map Z μ) fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)
⊢ covariance (mΩ := mΩ) X Y (Measure.map Z μ) = cov[X ∘ Z, Y ∘ Z; μ]

Tactic:
simp_rw [covariance, Function.comp_apply]

Premises used: ProbabilityTheory.covariance, Function.comp_apply
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
rw :
  Eq (α := ℝ)
    (∫ (x : Ω'),
      (X (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x) ∂μ)
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)
hφ : AEMeasurable Z μ
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (Measure.map Z μ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.map Z μ) fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
rw :
  Eq (α := ℝ)
    (∫ (x : Ω'),
      (X (Z x) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x) ∂μ)
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)
hφ : AEMeasurable Z μ
hfm : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
⊢ Eq (α := ℝ)
    (∫ (x : Ω'),
      (X (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x) ∂μ)
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ hφ : AEMeasurable Z μ
hfm : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
⊢ Eq (α := ℝ)
    (∫ (x : Ω'),
      (X (Z x) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z x) - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x) ∂μ)
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ hφ : AEMeasurable Z μ
hfm : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hφ₁ : AEMeasurable Z μ
hfm₁ : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hφ₂ : AEMeasurable Z μ
hfm₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (Measure.map Z μ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.map Z μ) fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ)

Tactic:
repeat rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

Tactic:
assumption
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)

Tactic:
assumption
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)

Tactic:
assumption
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (Measure.map Z μ)

Tactic:
(hX.sub aestronglyMeasurable_const).mul (hY.sub aestronglyMeasurable_const)

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.AEStronglyMeasurable.mul