awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ IsGaussian (multivariateGaussian μ S)
have h : Eq (α := (x : 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 ℝ ι))
  ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
    (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
          EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
      (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
Tactic: have h : (fun x ↦ μ + (toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S)) x) =
    (fun x ↦ μ + x) ∘ ((toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S))) := rfl
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h :
  Eq (α := (x : 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 ℝ ι))
    ((fun (x : EuclideanSpace ℝ ι) ↦ μ + x) ∘
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι))
⊢ IsGaussian.{u_1} (E := EuclideanSpace ℝ ι) (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
    (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 ℝ ι)))
have rw : IsGaussian (E := EuclideanSpace ℝ ι) (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
  (Measure.map (fun (x : EuclideanSpace ℝ ι) ↦ μ + x)
    (Measure.map (α := EuclideanSpace ℝ ι)
      (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
        (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
      (stdGaussian (EuclideanSpace ℝ ι))))
Tactic: rw [h, ← Measure.map_map (measurable_const_add μ) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ
have rw : (Measure.real.{u_1} (α := EuclideanSpace ℝ ι) (m := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
        (stdGaussian (EuclideanSpace ℝ ι)) Set.univ •
      μ +
    @integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι))
      fun (a : EuclideanSpace ℝ ι) ↦
      (((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
            EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
          (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
        a) =
  μ
Tactic: rw [multivariateGaussian, integral_map (by fun_prop) (by fun_prop),
    integral_add (integrable_const _), integral_const]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
rw :
  (Measure.real.{u_1} (α := EuclideanSpace ℝ ι) (m := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
          (stdGaussian (EuclideanSpace ℝ ι)) Set.univ •
        μ +
      @integral _ _ _ _ (WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι))
        fun (a : EuclideanSpace ℝ ι) ↦
        (((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
              EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
            (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
          a) =
    μ
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ
have rw₁ : @Integrable (EuclideanSpace ℝ ι) _ _ (EuclideanSpace ℝ ι) (WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
  (⇑((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
        EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) :
    (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
  (stdGaussian (EuclideanSpace ℝ ι))
Tactic: rw [multivariateGaussian, integral_map (by fun_prop) (by fun_prop),
    integral_add (integrable_const _), integral_const]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
⊢ (((covarianceBilin (multivariateGaussian μ S) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι →L[ℝ] ℝ) x :
          EuclideanSpace ℝ ι →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ι) → ℝ)
      y =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp
have 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 ℝ ι)
Tactic: have h : (fun x ↦ μ + x) ∘ ((toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S))) =
    (fun x ↦ μ + (toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S)) x) := rfl
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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 ℝ ι)
⊢ (((covarianceBilin (multivariateGaussian μ S) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι →L[ℝ] ℝ) x :
          EuclideanSpace ℝ ι →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ι) → ℝ)
      y =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp
have simp : (((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: simp only [multivariateGaussian]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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 ℝ ι)
⊢ (((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
have rw : IsSelfAdjoint (R := EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
  ((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) (CFC.sqrt S) :
    EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι)
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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 ℝ ι)
⊢ (((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
have h₁ : MemLp.{u_1, u_1} (α := EuclideanSpace ℝ ι) (m0 := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) id 2
  (stdGaussian (EuclideanSpace ℝ ι))
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i_1 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⟫
have h : ∀ (x : EuclideanSpace ℝ ι), x.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
⊢ cov[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i, fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp j; multivariateGaussian μ S] =
    S i j
have 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⟫
Tactic: have (i : ι) : (fun x : EuclideanSpace ℝ ι ↦ x i) =
      fun x ↦ ⟪EuclideanSpace.basisFun ι ℝ i, x⟫ := by ext; simp [PiLp.inner_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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⟫
⊢ cov[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i, fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp j; multivariateGaussian μ S] =
    S i j
have rw : ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i) ⬝ᵥ
    S *ᵥ ofLp (p := 2) ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j) =
  S i j
Tactic: rw [this, this, ← covarianceBilin_apply_eq_cov, covarianceBilin_multivariateGaussian hS]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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
⊢ cov[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i, fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp j; multivariateGaussian μ S] =
    S i j
have h : MemLp id 2 (multivariateGaussian μ S)
Tactic: rw [this, this, ← covarianceBilin_apply_eq_cov, covarianceBilin_multivariateGaussian hS]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Var[fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i; multivariateGaussian μ S] = S i i
have rw : AEMeasurable (β := ℝ) (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S)
Tactic: rw [← covariance_self, covariance_eval_multivariateGaussian hS]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Measure.map (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S) =
    gaussianReal (μ.ofLp i) (S i i).toNNReal
have 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
Tactic: rw [← EuclideanSpace.coe_proj, IsGaussian.map_eq_gaussianReal,
      ContinuousLinearMap.integral_comp_id_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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
⊢ Measure.map (fun (x : EuclideanSpace ℝ ι) ↦ x.ofLp i) (multivariateGaussian μ S) =
    gaussianReal (μ.ofLp i) (S i i).toNNReal
have h : Integrable id (multivariateGaussian μ S)
Tactic: rw [← EuclideanSpace.coe_proj, IsGaussian.map_eq_gaussianReal,
      ContinuousLinearMap.integral_comp_id_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ 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 : ι) ⋯))
have 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 : ι) sorry) fun (i : ↥J) ↦
        Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry))
Tactic: apply IsGaussian.ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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 : ι) ⋯))
⊢ 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 : ι) ⋯))
have 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 : ι) sorry) fun (i : ↥J) ↦
        Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry)))
Tactic: apply IsGaussian.ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ 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 : ι) ⋯))
have 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)
Tactic: simp only [id_eq, integral_id_multivariateGaussian]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ 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)
have hm : Integrable id (multivariateGaussian μ S)
Tactic: rw [ContinuousLinearMap.integral_id_map, integral_id_multivariateGaussian]