awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 ℝ ι
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
have (i : ι) := (hX i).aemeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 ω) μ
h :
  MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
    (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; μ] : ℝ)

Tactic:
nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]

Premises used: Real, ProbabilityTheory.covarianceBilin_apply_eq_cov, EuclideanSpace.basisFun, OrthonormalBasis.sum_repr', ProbabilityTheory.covariance_map_fun
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
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; μ]
⊢ 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; μ]

Tactic:
simp_rw [sum_inner, real_inner_smul_left, basisFun_inner]

Premises used: sum_inner, EuclideanSpace.basisFun_inner, real_inner_smul_left
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 μ
hY : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.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; μ]

Tactic:
rw [covariance_fun_sum_fun_sum]

Premises used: ProbabilityTheory.covariance_fun_sum_fun_sum
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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; μ])

Tactic:
Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
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; μ]
⊢ 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:
refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
rw : x.ofLp i * (y.ofLp j * cov[X i, X j; μ]) = x.ofLp i * y.ofLp j * cov[X i, X 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:
rw [covariance_const_mul_left, covariance_const_mul_right]

Premises used: ProbabilityTheory.covariance_const_mul_right, ProbabilityTheory.covariance_const_mul_left
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
⊢ x.ofLp i * (y.ofLp j * cov[X i, X j; μ]) = x.ofLp i * y.ofLp j * cov[X i, X j; μ]

Tactic:
ring
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 μ

Tactic:
fun i ↦ (hX i).const_mul _

Premises used: MeasureTheory.MemLp.const_mul, WithLp.ofLp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 μ

Tactic:
exact fun i ↦ (hX i).const_mul _

Premises used: MeasureTheory.MemLp.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * X i ω) 2 μ

Tactic:
fun i ↦ (hX i).const_mul _

Premises used: MeasureTheory.MemLp.const_mul, WithLp.ofLp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * X i ω) 2 μ

Tactic:
exact fun i ↦ (hX i).const_mul _

Premises used: MeasureTheory.MemLp.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 (ι → ℝ))
funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪x, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 (ι → ℝ))
funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ)) (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪y, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
⊢ AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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) μ
⊢ MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 (MemLp.of_eval_piLp hX)

Premises used: Iff.mpr, aestronglyMeasurable_id, MeasureTheory.MemLp.of_eval_piLp, MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
⊢ Eq.{u_1 + 1} (α := E →L[ℝ] E) (covarianceOperator 0) 0

Tactic:
simp [covarianceOperator]

Premises used: ProbabilityTheory.covarianceOperator
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 μ
h : ∀ (x : E), Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
⊢ Eq (α := E →L[ℝ] E) (covarianceOperator μ) 0

Tactic:
ext x
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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)

Tactic:
(unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm

Premises used: InnerProductSpace.unique_continuousLinearMapOfBilin, Eq.symm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
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
⊢ Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)

Tactic:
refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm

Premises used: InnerProductSpace.unique_continuousLinearMapOfBilin, Eq.symm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
⊢ ⟪(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:
simp [hμ, uncenteredCovarianceBilinDual_of_not_memLp]

Premises used: ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 μ : (a : E) → E) x, y⟫ = ∫ (z : E), ⟪x, z⟫ * ⟪y, z⟫ ∂μ

Tactic:
simp [covarianceOperator, uncenteredCovarianceBilinDual_apply hμ]

Premises used: ProbabilityTheory.uncenteredCovarianceBilinDual_apply, ProbabilityTheory.covarianceOperator
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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)

Tactic:
(unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm

Premises used: InnerProductSpace.unique_continuousLinearMapOfBilin, Eq.symm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
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
⊢ Eq (α := E) ((covarianceOperator μ : (a : E) → E) x : E) (∫ (y : E), ⟪x, y⟫ • y ∂μ : E)

Tactic:
refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm

Premises used: InnerProductSpace.unique_continuousLinearMapOfBilin, Eq.symm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 :
      ℝ)
hf : Integrable (ε := E) (fun (y : E) ↦ ⟪x, y⟫ • 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

Tactic:
rw [real_inner_comm, ← integral_inner]

Premises used: integral_inner, real_inner_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
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⟫
⊢ 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:
simp_rw [inner_smul_right, ← continuousLinearMapOfBilin_apply, ← covarianceOperator_inner hμ]

Premises used: ProbabilityTheory.covarianceOperator_inner, inner_smul_right, InnerProductSpace.continuousLinearMapOfBilin_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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 μ : (a : E) → E) x, y⟫ =
    ⟪(continuousLinearMapOfBilin
            (ContinuousLinearMap.bilinearComp (uncenteredCovarianceBilinDual μ)
              (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))
              (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E))) :
          (a : E) → E)
        x,
      y⟫

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
⊢ Integrable (ε := E) (fun (y : E) ↦ ⟪x, y⟫ • y) μ

Tactic:
memLp_one_iff_integrable.1 <| hμ.smul (hμ.const_inner x)

Premises used: MeasureTheory.MemLp.smul, MeasureTheory.MemLp.const_inner, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
⊢ Integrable (ε := E) (fun (y : E) ↦ ⟪x, y⟫ • y) μ

Tactic:
exact memLp_one_iff_integrable.1 <| hμ.smul (hμ.const_inner x)

Premises used: MeasureTheory.MemLp.smul, MeasureTheory.MemLp.const_inner, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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)
neg : ∀ (hμ : ¬MemLp id 2 μ), LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)

Tactic:
by_cases hμ : MemLp id 2 μ

Premises used: id, MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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)

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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)

Tactic:
⟨fun x y ↦ ?_, fun x ↦ ?_⟩

Premises used: LinearMap.IsPositive, And.intro
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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⟫
pos₁ :
  ∀ (x : E),
    LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, x⟫ : ℝ)
⊢ LinearMap.IsPositive (↑(covarianceOperator μ) : E →ₗ[ℝ] E)

Tactic:
refine ⟨fun x y ↦ ?_, fun x ↦ ?_⟩
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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⟫
pos₂ : Eq (α := ℝ) (∫ (z : E), ⟪x, z⟫ * ⟪y, z⟫ ∂μ) (∫ (z : E), ⟪y, z⟫ * ⟪x, z⟫ ∂μ)
⊢ ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, y⟫ =
    ⟪x, ((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) y⟫

Tactic:
simp_rw [ContinuousLinearMap.coe_coe, real_inner_comm _ x, covarianceOperator_inner hμ,
      mul_comm]

Premises used: ContinuousLinearMap.coe_coe, ProbabilityTheory.covarianceOperator_inner, mul_comm, real_inner_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
pos : LE.le (α := ℝ) 0 (∫ (z : E), HPow.hPow (β := ℕ) ⟪x, z⟫ 2 ∂μ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, x⟫ : ℝ)

Tactic:
simp only [ContinuousLinearMap.coe_coe, covarianceOperator_inner hμ, ← pow_two,
      RCLike.re_to_real]

Premises used: pow_two, ContinuousLinearMap.coe_coe, RCLike.re_to_real, ProbabilityTheory.covarianceOperator_inner