awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
nth_rw :
  cov[fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω),
      fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω);
      μ] =
    ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have hX₁ : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫)
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
nth_rw :
  cov[fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω),
      fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω);
      μ] =
    ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
hX₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have hY : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫)
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
nth_rw :
  cov[fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω),
      fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω);
      μ] =
    ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
hX₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
hY :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have hZ : AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ
Tactic: nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
nth_rw :
  cov[fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω),
      fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω);
      μ] =
    ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
hX₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
hY :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
hZ : AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have h : MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω),
      fun (ω : Ω) ↦
      inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
        (∑ i : ι,
          HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        (toLp 2 fun (x : ι) ↦ X x ω);
      μ] =
    ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
have simp_rw : cov[fun (ω : Ω) ↦ ∑ x_1 : ι, x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ ∑ x : ι, y.ofLp x * X x ω; μ] =
  ∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
Tactic: simp_rw [sum_inner, real_inner_smul_left, basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun (ω : Ω) ↦ ∑ x_1 : ι, x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ ∑ x : ι, y.ofLp x * X x ω; μ] =
    ∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
have rw : Eq (α := ℝ) (∑ i : ι, ∑ j : ι, cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ])
  (∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ])
Tactic: rw [covariance_fun_sum_fun_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
rw :
  Eq (α := ℝ) (∑ i : ι, ∑ j : ι, cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ])
    (∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ])
⊢ cov[fun (ω : Ω) ↦ ∑ x_1 : ι, x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ ∑ x : ι, y.ofLp x * X x ω; μ] =
    ∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
have hX₁ : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 μ
Tactic: rw [covariance_fun_sum_fun_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
rw :
  Eq (α := ℝ) (∑ i : ι, ∑ j : ι, cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ])
    (∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ])
hX₁ : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 μ
⊢ cov[fun (ω : Ω) ↦ ∑ x_1 : ι, x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ ∑ x : ι, y.ofLp x * X x ω; μ] =
    ∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
have hY : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * X i ω) 2 μ
Tactic: rw [covariance_fun_sum_fun_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ Eq (α := ℝ) (∑ i : ι, ∑ j : ι, cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ])
    (∑ x_1 : ι, ∑ x_2 : ι, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ])
have refine : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    ∀ (j : ι),
      Membership.mem (γ := Finset ι) Finset.univ j →
        cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ] = x.ofLp i * y.ofLp j * cov[X i, X j; μ]
Tactic: refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
j : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ j
⊢ cov[fun (ω : Ω) ↦ x.ofLp i * X i ω, fun (ω : Ω) ↦ y.ofLp j * X j ω; μ] = x.ofLp i * y.ofLp j * cov[X i, X j; μ]
have rw : x.ofLp i * (y.ofLp j * cov[X i, X j; μ]) = x.ofLp i * y.ofLp j * cov[X i, X j; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫
Tactic: fun_prop
-- 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
inst_4 : CompleteSpace E
hμ : ¬MemLp id 2 μ
⊢ Eq (α := E →L[ℝ] E) (covarianceOperator μ) 0
have h : ∀ (x : E), Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
Tactic: ext x
-- 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
inst_4 : CompleteSpace E
hμ : ¬MemLp id 2 μ
x : E
⊢ Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
have h : ∀ (y : E),
  ⟪(0 : (a : E) → E) x, y⟫ =
    (((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
              (a : E) → E →L[ℝ] ℝ)
            x :
          E →L[ℝ] ℝ) :
        (a : E) → ℝ)
      y
Tactic: refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x : E
⊢ Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) (∫ (y : E), ⟪x, y⟫ • y ∂μ : E)
have refine : ∀ (y : E),
  ⟪∫ (y : E), ⟪x, y⟫ • y ∂μ, y⟫ =
    (((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
              (a : E) → E →L[ℝ] ℝ)
            x :
          E →L[ℝ] ℝ) :
        (a : E) → ℝ)
      y
Tactic: refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪∫ (y : E), ⟪x, y⟫ • y ∂μ, y⟫ =
    (((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
              (a : E) → E →L[ℝ] ℝ)
            x :
          E →L[ℝ] ℝ) :
        (a : E) → ℝ)
      y
have rw : Eq (α := ℝ) (∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ : ℝ)
  ((((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
              (a : E) → E →L[ℝ] ℝ)
            x :
          E →L[ℝ] ℝ) :
        (a : E) → ℝ)
      y :
    ℝ)
Tactic: rw [real_inner_comm, ← integral_inner]
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
rw :
  Eq (α := ℝ) (∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ : ℝ)
    ((((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                  (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                  (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
                (a : E) → E →L[ℝ] ℝ)
              x :
            E →L[ℝ] ℝ) :
          (a : E) → ℝ)
        y :
      ℝ)
⊢ ⟪∫ (y : E), ⟪x, y⟫ • y ∂μ, y⟫ =
    (((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
              (a : E) → E →L[ℝ] ℝ)
            x :
          E →L[ℝ] ℝ) :
        (a : E) → ℝ)
      y
have hf : Integrable (ε := E) (fun (y : E) ↦ ⟪x, y⟫ • y) μ
Tactic: rw [real_inner_comm, ← integral_inner]
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ Eq (α := ℝ) (∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ : ℝ)
    ((((ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
                  (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
                  (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) :
                (a : E) → E →L[ℝ] ℝ)
              x :
            E →L[ℝ] ℝ) :
          (a : E) → ℝ)
        y :
      ℝ)
have simp_rw : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ =
  ⟪(continuousLinearMapOfBilin
          (ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
            (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
            (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))) :
        (a : E) → E)
      x,
    y⟫
Tactic: simp_rw [inner_smul_right, ← continuousLinearMapOfBilin_apply, ← covarianceOperator_inner hμ]
-- 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
inst_4 : CompleteSpace E
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
have pos : ∀ (hμ : MemLp id 2 μ), LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
Tactic: by_cases hμ : MemLp id 2 μ
-- 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
inst_4 : CompleteSpace E
pos : ∀ (hμ : MemLp id 2 μ), LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
have neg : ∀ (hμ : ¬MemLp id 2 μ), LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
Tactic: by_cases hμ : MemLp id 2 μ
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
have pos : ∀ (x y : E),
  ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
    ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫
Tactic: refine ⟨fun x y ↦ ?_, fun x ↦ ?_⟩
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
pos :
  ∀ (x y : E),
    ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
      ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
have pos₁ : ∀ (x : E),
  LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨fun x y ↦ ?_, fun x ↦ ?_⟩
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
    ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫
have pos : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ = ⟪x, (covarianceOperator μ : (a : E) → E) y⟫
Tactic: simp_rw [ContinuousLinearMap.coe_coe, real_inner_comm _ x, covarianceOperator_inner hμ,
      mul_comm]
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
pos : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ = ⟪x, (covarianceOperator μ : (a : E) → E) y⟫
⊢ ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
    ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫
have pos₁ : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ = ⟪(covarianceOperator μ : (a : E) → E) y, x⟫
Tactic: simp_rw [ContinuousLinearMap.coe_coe, real_inner_comm _ x, covarianceOperator_inner hμ,
      mul_comm]
-- 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
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
pos : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ = ⟪x, (covarianceOperator μ : (a : E) → E) y⟫
pos₁ : ⟪(covarianceOperator μ : (a : E) → E) x, y⟫ = ⟪(covarianceOperator μ : (a : E) → E) y, x⟫
⊢ ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
    ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫
have pos₂ : Eq (α := ℝ) (∫ (z : E), ⟪x, z⟫ * ⟪y, z⟫ ∂μ) (∫ (z : E), ⟪y, z⟫ * ⟪x, z⟫ ∂μ)
Tactic: simp_rw [ContinuousLinearMap.coe_coe, real_inner_comm _ x, covarianceOperator_inner hμ,
      mul_comm]