awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
⊢ Measurable (α := EuclideanSpace ℝ ι) (β := EuclideanSpace ℝ ι)
    (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
          EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
      (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
rw :
  IsSelfAdjoint (R := EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
    ((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
      EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
h₁ :
  MemLp.{u_1, u_1} (α := EuclideanSpace ℝ ι) (m0 := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) id 2
    (stdGaussian (EuclideanSpace ℝ ι))
⊢ (((covarianceBilin
                (Measure.map
                  (fun (x : EuclideanSpace ℝ ι) ↦
                    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
                      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
                                (CFC.sqrt S) :
                              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
                            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                          x :
                        EuclideanSpace ℝ ι))
                  (stdGaussian (EuclideanSpace ℝ ι))) :
              (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι →L[ℝ] ℝ)
            x :
          EuclideanSpace ℝ ι →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ι) → ℝ)
      y =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp

Tactic:
rw [← h, ← Measure.map_map (measurable_const_add μ) (by fun_prop), covarianceBilin_map_const_add,
    covarianceBilin_map, covarianceBilin_stdGaussian, innerSL_apply_apply,
    ContinuousLinearMap.adjoint_inner_left, IsSelfAdjoint.adjoint_eq,
    ← ContinuousLinearMap.comp_apply, ← ContinuousLinearMap.mul_def, ← map_mul,
      CFC.sqrt_mul_sqrt_self _ hS.nonneg, inner_toEuclideanCLM]

Premises used: innerSL_apply_apply, IsSelfAdjoint.adjoint_eq, MeasurableAdd.measurable_const_add, ProbabilityTheory.covarianceBilin_stdGaussian, ContinuousLinearMap.adjoint_inner_left, Matrix.PosSemidef.nonneg, Matrix.inner_toEuclideanCLM, map_mul, ProbabilityTheory.covarianceBilin_map, ContinuousLinearMap.mul_def, ProbabilityTheory.covarianceBilin_map_const_add, MeasureTheory.Measure.map_map, CFC.sqrt_mul_sqrt_self, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
⊢ IsSelfAdjoint (R := EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
    ((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
      EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)

Tactic:
(CFC.sqrt_nonneg S).isSelfAdjoint.map _

Premises used: LE.le.isSelfAdjoint, IsSelfAdjoint.map, CFC.sqrt_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
⊢ IsSelfAdjoint (R := EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
    ((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
      EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)

Tactic:
exact (CFC.sqrt_nonneg S).isSelfAdjoint.map _

Premises used: LE.le.isSelfAdjoint, IsSelfAdjoint.map, CFC.sqrt_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
⊢ MemLp.{u_1, u_1} (α := EuclideanSpace ℝ ι) (m0 := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) id 2
    (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h :
  Eq (α := EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
    fun (x : EuclideanSpace ℝ ι) ↦
    HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
      ((((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          x :
        EuclideanSpace ℝ ι)
⊢ MemLp.{u_1, u_1} (α := EuclideanSpace ℝ ι) (m0 := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) id 2
    (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
exact IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i_1 j i : ι
h : ∀ (x : EuclideanSpace ℝ ι), x.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
⊢ Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
    fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i_1 j i : ι
x : EuclideanSpace ℝ ι
⊢ x.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫

Tactic:
simp [PiLp.inner_apply]

Premises used: PiLp.inner_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
⊢ ∀ (i : ι),
    Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
      fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫

Tactic:
have (i : ι) : (fun x : EuclideanSpace ℝ ι ↦ x i) =
      fun x ↦ ⟪EuclideanSpace.basisFun ι ℝ i, x⟫ := by ext; simp [PiLp.inner_apply]
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
      fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
rw :
  ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) ⬝ᵥ
      S *ᵥ ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j) =
    S i j
h : MemLp id 2 (multivariateGaussian μ S)
⊢ cov[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i, fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp j; multivariateGaussian μ S] =
    S i j

Tactic:
rw [this, this, ← covarianceBilin_apply_eq_cov, covarianceBilin_multivariateGaussian hS]

Premises used: ProbabilityTheory.covarianceBilin_multivariateGaussian, ProbabilityTheory.covarianceBilin_apply_eq_cov
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
      fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
⊢ ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) ⬝ᵥ
      S *ᵥ ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j) =
    S i j

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
      fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := (x : EuclideanSpace ℝ ι) → (fun (x : ι) ↦ ℝ) i) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i)
      fun (x : EuclideanSpace ℝ ι) ↦ ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
exact IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
rw : AEMeasurable (β := ℝ) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S)
⊢ Var[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i; multivariateGaussian μ S] = S i i

Tactic:
rw [← covariance_self, covariance_eval_multivariateGaussian hS]

Premises used: ProbabilityTheory.covariance_eval_multivariateGaussian, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Measurable (β := ℝ) fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ AEMeasurable (β := ℝ) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S)

Tactic:
exact Measurable.aemeasurable <| by fun_prop

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
rw :
  gaussianReal
      ((EuclideanSpace.proj i : (a : EuclideanSpace ℝ ι) → ℝ) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[(⇑(EuclideanSpace.proj i) : (a : EuclideanSpace ℝ ι) → ℝ); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal
h : Integrable id (multivariateGaussian μ S)
⊢ Measure.map (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S) =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

Tactic:
rw [← EuclideanSpace.coe_proj, IsGaussian.map_eq_gaussianReal,
      ContinuousLinearMap.integral_comp_id_comm]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal, EuclideanSpace.coe_proj, ContinuousLinearMap.integral_comp_id_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal
      ((EuclideanSpace.proj i : (a : EuclideanSpace ℝ ι) → ℝ) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[(⇑(EuclideanSpace.proj i) : (a : EuclideanSpace ℝ ι) → ℝ); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

Tactic:
simp [variance_eval_multivariateGaussian hS]

Premises used: ProbabilityTheory.variance_eval_multivariateGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
exact IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x : EuclideanSpace ℝ ι
⊢ charFun (multivariateGaussian μ S) x = cexp ((↑⟪x, μ⟫ : ℂ) * I - (↑(x.ofLp ⬝ᵥ S *ᵥ x.ofLp) : ℂ) / 2)

Tactic:
simp [IsGaussian.charFun_eq', covarianceBilin_multivariateGaussian hS]

Premises used: ProbabilityTheory.covarianceBilin_multivariateGaussian, ProbabilityTheory.IsGaussian.charFun_eq'
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Measurable (α := EuclideanSpace ℝ ↥I) (β := EuclideanSpace ℝ ↥J)
    (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
hm :
  Eq (α := EuclideanSpace ℝ ↥J)
    (@integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S))
      fun (x : EuclideanSpace ℝ ↥J) ↦ id x)
    (∫ (x : EuclideanSpace ℝ ↥J),
      id
        x ∂multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))
hv :
  Eq (α := EuclideanSpace ℝ ↥J →L[ℝ] EuclideanSpace ℝ ↥J →L[ℝ] ℝ)
    (covarianceBilin
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S)))
    (covarianceBilin
      (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)))
⊢ Eq (α := Measure (EuclideanSpace ℝ ↥J))
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
      (multivariateGaussian μ S))
    (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
      (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
        Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))

Tactic:
apply IsGaussian.ext

Premises used: ProbabilityTheory.IsGaussian.ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
hm :
  Eq (α := EuclideanSpace ℝ ↥J)
    (@integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
        (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
          (multivariateGaussian μ S))
        fun (x : EuclideanSpace ℝ ↥J) ↦ x :
      EuclideanSpace ℝ ↥J)
    ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ : EuclideanSpace ℝ ↥J)
⊢ Eq (α := EuclideanSpace ℝ ↥J)
    (@integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S))
      fun (x : EuclideanSpace ℝ ↥J) ↦ id x)
    (∫ (x : EuclideanSpace ℝ ↥J),
      id
        x ∂multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))

Tactic:
simp only [id_eq, integral_id_multivariateGaussian]

Premises used: ProbabilityTheory.integral_id_multivariateGaussian, id_eq
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
hm : Integrable id (multivariateGaussian μ S)
⊢ Eq (α := EuclideanSpace ℝ ↥J)
    (@integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
        (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
          (multivariateGaussian μ S))
        fun (x : EuclideanSpace ℝ ↥J) ↦ x :
      EuclideanSpace ℝ ↥J)
    ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ : EuclideanSpace ℝ ↥J)

Tactic:
rw [ContinuousLinearMap.integral_id_map, integral_id_multivariateGaussian]

Premises used: ProbabilityTheory.integral_id_multivariateGaussian, ContinuousLinearMap.integral_id_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
exact IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
hv :
  Eq (α := LinearMap.BilinForm ℝ (EuclideanSpace ℝ ↥J))
    (ContinuousLinearMap.toBilinForm
      (covarianceBilin
        (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
          (multivariateGaussian μ S))))
    (ContinuousLinearMap.toBilinForm
      (covarianceBilin
        (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
          (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
            Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))))
⊢ Eq (α := EuclideanSpace ℝ ↥J →L[ℝ] EuclideanSpace ℝ ↥J →L[ℝ] ℝ)
    (covarianceBilin
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S)))
    (covarianceBilin
      (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)))

Tactic:
rw [← ContinuousLinearMap.toBilinForm_inj]

Premises used: ContinuousLinearMap.toBilinForm_inj