Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ cov[(fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI),
      (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI);
      multivariateGaussian μ S] =
    ((covarianceBilin
          (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)))
        ((EuclideanSpace.basisFun ↥J ℝ).toBasis i))
      ((EuclideanSpace.basisFun ↥J ℝ).toBasis j)

pp: case hv.hX
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hY
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

pp: case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

Tactic:
]

Goal state after:
case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ cov[(fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI),
      (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI);
      multivariateGaussian μ S] =
    ((covarianceBilin
          (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩)))
        ((EuclideanSpace.basisFun ↥J ℝ).toBasis i))
      ((EuclideanSpace.basisFun ↥J ℝ).toBasis j)

case hv.hX
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

case hv.hY
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))