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 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; μ]
⊢ cov[X - Y, Z; μ] = cov[X, Z; μ] - cov[Y, Z; μ]
have simp_rw₁ : cov[X, Z; μ] + cov[-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]
-- 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 simp_rw : 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]
-- 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 μ
simp_rw : cov[X, Y + -Z; μ] = cov[X, Y; μ] + -cov[X, Z; μ]
⊢ cov[X, Y - Z; μ] = cov[X, Y; μ] - cov[X, Z; μ]
have simp_rw₁ : cov[X, Y; μ] + cov[X, -Z; μ] = cov[X, Y; μ] + -cov[X, Z; μ]
Tactic: simp_rw [sub_eq_add_neg, covariance_add_right hX hY hZ.neg, covariance_neg_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ cov[∑ i ∈ insert i s, X i, Y; μ] = ∑ i ∈ insert i s, cov[X i, Y; μ]
have insert : ∀ i ∈ s, MemLp (X i) 2 μ
Tactic: rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ cov[∑ i ∈ Insert.insert i s, X i, Y; μ] = ∑ i ∈ Insert.insert i s, cov[X i, Y; μ]
have insert₁ : MemLp (X i) 2 μ
Tactic: rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ cov[∑ i ∈ Insert.insert i s, X i, Y; μ] = ∑ i ∈ Insert.insert i s, cov[X i, Y; μ]
have insert₂ : MemLp (ε := ℝ) (∑ x ∈ s, X x) 2 μ
Tactic: rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
have empty : ∀ (hX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (X i) 2 μ),
  cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
have 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 i s, MemLp (X i_1) 2 μ), cov[∑ i ∈ insert i s, X i, Y; μ] = ∑ i ∈ insert 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
have empty : ∀ (hX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (X i) 2 μ),
  cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
⊢ cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
have 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 i s, MemLp (X i_1) 2 μ), cov[∑ i ∈ insert i s, X i, Y; μ] = ∑ i ∈ insert 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! covariance_sum_left' hX hY
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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[fun (ω : Ω) ↦ ∑ i : ι, X i ω, Y; μ] = ∑ i : ι, cov[X i, Y; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
Tactic: convert! covariance_sum_left hX hY
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
have rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, Y; μ]) (∑ i ∈ s, cov[Y, X i; μ])
Tactic: rw [covariance_comm, covariance_sum_left' hX hY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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, fun (ω : Ω) ↦ ∑ i ∈ s, X i ω; μ] = ∑ i ∈ s, cov[Y, X i; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! covariance_sum_right' hX hY
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ]
have rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ]) (∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ])
Tactic: rw [covariance_sum_left' hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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; μ])
⊢ cov[∑ i ∈ s, X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]
have rw₁ : MemLp (ε := ℝ) (∑ j ∈ t, Y j) 2 μ
Tactic: rw [covariance_sum_left' hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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
⊢ cov[X i, ∑ j ∈ t, Y j; μ] = ∑ j ∈ t, cov[X i, Y j; μ]
have rw : Eq (α := ℝ) (∑ i_1 ∈ t, cov[X i, Y i_1; μ]) (∑ j ∈ t, cov[X i, Y j; μ])
Tactic: rw [covariance_sum_right' hY (hX i hi)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω, fun (ω : Ω) ↦ ∑ j ∈ t, Y j ω; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! covariance_sum_sum' hX hY
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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)
⊢ cov[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω, fun (ω : Ω) ↦ ∑ j ∈ t, Y j ω; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]
have h₁ : ∀ (x : Ω), Eq (α := ℝ) (∑ j ∈ t, Y j x) ((∑ j ∈ t, Y j) x)
Tactic: convert! covariance_sum_sum' hX hY
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
⊢ covariance (mΩ := mΩ) X Y (Measure.map (⇑Z : (a : Ω') → Ω) μ) =
    cov[X ∘ (⇑Z : (a : Ω') → Ω), Y ∘ (⇑Z : (a : Ω') → Ω); μ]
have 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 ∂μ) ∂μ)
Tactic: simp_rw [covariance, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 ∂μ) ∂μ)
⊢ covariance (mΩ := mΩ) X Y (Measure.map (⇑Z : (a : Ω') → Ω) μ) =
    cov[X ∘ (⇑Z : (a : Ω') → Ω), Y ∘ (⇑Z : (a : Ω') → Ω); μ]
have 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 ∂μ) ∂μ)
Tactic: simp_rw [covariance, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ covariance (mΩ := mΩ) X Y (Measure.map Z μ) = cov[X ∘ Z, Y ∘ Z; μ]
have 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) ∂μ) ∂μ)
Tactic: simp_rw [covariance, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ 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) ∂μ) ∂μ)
have 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) ∂μ) ∂μ)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ 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) ∂μ) ∂μ)
have 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 μ)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ 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) ∂μ) ∂μ)
have 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) ∂μ) ∂μ)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
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 μ
⊢ 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) ∂μ) ∂μ)
have 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 μ)
Tactic: repeat rw [integral_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, Y; μ] = 0
have pos : ∀ (h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0), cov[X, Y; μ] = 0
Tactic: by_cases h' : ∀ᵐ ω ∂μ, X ω = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
pos : ∀ (h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0), cov[X, Y; μ] = 0
⊢ cov[X, Y; μ] = 0
have neg : ∀ (h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0), cov[X, Y; μ] = 0
Tactic: by_cases h' : ∀ᵐ ω ∂μ, X ω = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0
have pos : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)) 0
Tactic: refine integral_eq_zero_of_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)) 0
have h₁ : ∀ (ω : Ω) (hω : X ω = 0), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = 0 ω
Tactic: filter_upwards [h'] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0
have this : IsProbabilityMeasure μ
Tactic: have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
⊢ cov[X, Y; μ] = 0
have neg : ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) = 0
Tactic: rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral
       hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
neg : ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) = 0
⊢ cov[X, Y; μ] = 0
have neg₁ : HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) -
    HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) =
  0
Tactic: rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral
       hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
neg : ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) = 0
neg₁ :
  HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) -
      HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) =
    0
⊢ cov[X, Y; μ] = 0
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral
       hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
h : ¬MemLp id 2 μ
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) 0
have h₁ : ∀ (x x_1 : E),
  Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
    ((((0 : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
x y : E
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
have rw : Eq (α := ℝ)
  ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
    ℝ)
  ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
Tactic: rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
    covarianceBilin_eq_covarianceBilinDual]