awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
apply :
  Eq.{u_1 + 1} (α := (t : EuclideanSpace ℝ ι) → ℂ)
    (charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
      (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1)))
    (charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι)))
⊢ Eq.{u_1 + 1} (α := Measure (WithLp 2 ((i : ι) → ℝ)))
    (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1))
    (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
apply Measure.ext_of_charFun (E := EuclideanSpace ℝ ι)

Premises used: MeasureTheory.Measure.ext_of_charFun
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
h :
  ∀ (t : EuclideanSpace ℝ ι),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
        (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1)) t =
      charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι)) t
⊢ Eq.{u_1 + 1} (α := (t : EuclideanSpace ℝ ι) → ℂ)
    (charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
      (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1)))
    (charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι)))

Tactic:
ext t
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
t : EuclideanSpace ℝ ι
h :
  cexp (∑ x : ι, ((↑(t.ofLp x) : ℂ) * (↑0 : ℂ) * I - (↑(↑1 : ℝ) : ℂ) * (↑(HPow.hPow (β := ℕ) (t.ofLp x) 2) : ℂ) / 2)) =
    cexp (-(↑(∑ x : ι, HPow.hPow (β := ℕ) (t.ofLp x) 2) : ℂ) / 2)
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
      (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1)) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i)) (stdGaussian (EuclideanSpace ℝ ι)) t

Tactic:
simp_rw [charFun_stdGaussian, charFun_pi, charFun_gaussianReal, ← exp_sum, ← ofReal_pow,
    EuclideanSpace.real_norm_sq_eq]

Premises used: EuclideanSpace.real_norm_sq_eq, MeasureTheory.charFun_pi, ProbabilityTheory.charFun_stdGaussian, Complex.exp_sum, Complex.ofReal_pow, ProbabilityTheory.charFun_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
t : EuclideanSpace ℝ ι
⊢ cexp (∑ x : ι, ((↑(t.ofLp x) : ℂ) * (↑0 : ℂ) * I - (↑(↑1 : ℝ) : ℂ) * (↑(HPow.hPow (β := ℕ) (t.ofLp x) 2) : ℂ) / 2)) =
    cexp (-(↑(∑ x : ι, HPow.hPow (β := ℕ) (t.ofLp x) 2) : ℂ) / 2)

Tactic:
simp [Finset.sum_div, neg_div]

Premises used: neg_div, Finset.sum_div
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
simp_rw :
  Eq (α := (x : ι → ℝ) → E)
    (fun (x : ι → ℝ) ↦
      (OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι) : (a : EuclideanSpace ℝ ι) → E) (toLp 2 x))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))
⊢ Eq (α := (x : ι → ℝ) → E) (fun (x : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))

Tactic:
simp_rw [← b.equiv_apply_euclideanSpace]

Premises used: OrthonormalBasis.equiv_apply_euclideanSpace
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
⊢ Eq (α := (x : ι → ℝ) → E)
    (fun (x : ι → ℝ) ↦
      (OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι) : (a : EuclideanSpace ℝ ι) → E) (toLp 2 x))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
⊢ Eq (α := (x : ι → ℝ) → E) (fun (x : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))

Tactic:
have : (fun (x : ι → ℝ) ↦ ∑ i, x i • b i) =
      ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ (toLp 2) := by
    simp_rw [← b.equiv_apply_euclideanSpace]
    rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
this :
  Eq (α := (x : ι → ℝ) → E) (fun (x : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))
hg :
  Measurable.{u_1, u_2} (α := EuclideanSpace ℝ ι) (β := E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
hf : Measurable.{u_1, u_1} (α := (i : ι) → ℝ) (β := EuclideanSpace ℝ ι) (toLp 2)
⊢ Eq (α := Measure E) (stdGaussian E)
    (Measure.map (fun (x : (i : ι) → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
      (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1))

Tactic:
rw [this, ← Measure.map_map, map_pi_eq_stdGaussian, stdGaussian_map]

Premises used: ProbabilityTheory.map_pi_eq_stdGaussian, ProbabilityTheory.stdGaussian_map, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
this :
  Eq (α := (x : ι → ℝ) → E) (fun (x : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))
funProp :
  LE.le.{u_1} (α := MeasurableSpace (EuclideanSpace ℝ ι)) (WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
    (WithLp.measurableSpace 2 ((i : ι) → ℝ))
funProp₁ :
  MeasurableEmbedding.{u_1, u_2} (β := E) fun (a : EuclideanSpace ℝ ι) ↦
    (OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι) : (a : EuclideanSpace ℝ ι) → E) a
⊢ Measurable.{u_1, u_2} (α := EuclideanSpace ℝ ι) (β := E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : OrthonormalBasis ι ℝ E
this :
  Eq (α := (x : ι → ℝ) → E) (fun (x : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (x i) ((b : (a : ι) → E) i : E))
    (Function.comp (β := EuclideanSpace ℝ ι)
      (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
      (toLp 2))
⊢ Measurable.{u_1, u_1} (α := (i : ι) → ℝ) (β := EuclideanSpace ℝ ι) (toLp 2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : ¬S.PosSemidef
rw :
  Eq (α := Measure (EuclideanSpace ℝ ι))
    (Measure.map
      (fun (x : EuclideanSpace ℝ ι) ↦
        HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
          (((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) 0 :
                (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
              x :
            EuclideanSpace ℝ ι))
      (stdGaussian (EuclideanSpace ℝ ι)))
    (Measure.dirac μ)
ha : ¬0 ≤ S
⊢ multivariateGaussian μ S = Measure.dirac μ

Tactic:
rw [multivariateGaussian, CFC.sqrt, cfcₙ_apply_of_not_predicate]

Premises used: CFC.sqrt, cfcₙ_apply_of_not_predicate, ProbabilityTheory.multivariateGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : ¬S.PosSemidef
⊢ Eq (α := Measure (EuclideanSpace ℝ ι))
    (Measure.map
      (fun (x : EuclideanSpace ℝ ι) ↦
        HAdd.hAdd (β := EuclideanSpace ℝ ι) μ
          (((toEuclideanCLM : (a : Matrix ι ι ℝ) → EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι) 0 :
                (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
              x :
            EuclideanSpace ℝ ι))
      (stdGaussian (EuclideanSpace ℝ ι)))
    (Measure.dirac μ)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : ¬S.PosSemidef
⊢ ¬(S - 0).PosSemidef

Tactic:
simpa
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
⊢ Eq.{u_1 + 1} (α := Measure (EuclideanSpace ℝ ι)) (multivariateGaussian 0 1) (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
simp [multivariateGaussian]

Premises used: ProbabilityTheory.multivariateGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ 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
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 ℝ ι))
⊢ 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 ι ι ℝ
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 ℝ ι))
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 ℝ ι))))
⊢ 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 ℝ ι)))

Tactic:
rw [h, ← Measure.map_map (measurable_const_add μ) (by fun_prop)]

Premises used: MeasurableAdd.measurable_const_add, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 (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:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ AEMeasurable (β := EuclideanSpace ℝ ι) (_m := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
    (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 ℝ ι))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ AEStronglyMeasurable (β := EuclideanSpace ℝ ι) (m₀ := WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
    (fun (x : EuclideanSpace ℝ ι) ↦ x)
    (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 ℝ ι)))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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) =
    μ
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 ℝ ι))
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ

Tactic:
rw [multivariateGaussian, integral_map (by fun_prop) (by fun_prop),
    integral_add (integrable_const _), integral_const]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.multivariateGaussian, MeasureTheory.integral_const, MeasureTheory.integrable_const, MeasureTheory.integral_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ (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:
simp [ContinuousLinearMap.integral_comp_comm _ IsGaussian.integrable_fun_id]

Premises used: ProbabilityTheory.IsGaussian.integrable_fun_id, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ 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 ι ι ℝ
⊢ @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:
exact IsGaussian.integrable_id.comp_measurable (by fun_prop)

Premises used: MeasureTheory.Integrable.comp_measurable, ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), id x ∂multivariateGaussian μ S = μ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
⊢ 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
-- 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 ℝ ι)
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
⊢ (((covarianceBilin (multivariateGaussian μ S) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι →L[ℝ] ℝ) x :
          EuclideanSpace ℝ ι →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ι) → ℝ)
      y =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp

Tactic:
simp only [multivariateGaussian]

Premises used: ProbabilityTheory.multivariateGaussian