awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
t : E
simp_rw :
  cexp
      (∑ x : Fin (finrank ℝ E),
        -(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₁ :
  cexp
      (-∑ x : Fin (finrank ℝ E),
          HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₂ :
  cexp
      (-HDiv.hDiv (α := ℂ)
          (∑ i : Fin (finrank ℝ E),
            HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i, t⟫ : ℂ) 2)
          2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
⊢ ∏ x : Fin (finrank ℝ E),
      cexp (-(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
have simp_rw₃ : cexp
    (-HDiv.hDiv (α := ℂ)
        (∑ x : Fin (finrank ℝ E),
          (↑(HPow.hPow (β := ℕ) ⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ 2) : ℂ))
        2) =
  cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
Tactic: simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
t : E
simp_rw :
  cexp
      (∑ x : Fin (finrank ℝ E),
        -(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₁ :
  cexp
      (-∑ x : Fin (finrank ℝ E),
          HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₂ :
  cexp
      (-HDiv.hDiv (α := ℂ)
          (∑ i : Fin (finrank ℝ E),
            HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i, t⟫ : ℂ) 2)
          2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₃ :
  cexp
      (-HDiv.hDiv (α := ℂ)
          (∑ x : Fin (finrank ℝ E),
            (↑(HPow.hPow (β := ℕ) ⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ 2) : ℂ))
          2) =
    cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
⊢ ∏ x : Fin (finrank ℝ E),
      cexp (-(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
have simp_rw₄ : cexp
    (-((↑(∑ i : Fin (finrank ℝ E),
              HPow.hPow (β := ℕ) ⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i, t⟫ 2) :
          ℂ) /
        2)) =
  cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
Tactic: simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
t : E
simp_rw :
  cexp
      (∑ x : Fin (finrank ℝ E),
        -(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₁ :
  cexp
      (-∑ x : Fin (finrank ℝ E),
          HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₂ :
  cexp
      (-HDiv.hDiv (α := ℂ)
          (∑ i : Fin (finrank ℝ E),
            HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i, t⟫ : ℂ) 2)
          2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
simp_rw₃ :
  cexp
      (-HDiv.hDiv (α := ℂ)
          (∑ x : Fin (finrank ℝ E),
            (↑(HPow.hPow (β := ℕ) ⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ 2) : ℂ))
          2) =
    cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
simp_rw₄ :
  cexp
      (-((↑(∑ i : Fin (finrank ℝ E),
                HPow.hPow (β := ℕ) ⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i, t⟫ 2) :
            ℂ) /
          2)) =
    cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
⊢ ∏ x : Fin (finrank ℝ E),
      cexp (-(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
have simp_rw₅ : cexp (-((↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)) = cexp (-(↑(HPow.hPow (β := ℕ) ‖t‖ 2) : ℂ) / 2)
Tactic: simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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
⊢ IsGaussian (mE := inst_4) (stdGaussian E)
have refine : ∀ (t : E),
  charFun (mE := inst_4) (stdGaussian E) t =
    cexp ((↑⟪t, 0⟫ : ℂ) * I - (↑((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
Tactic: refine isGaussian_iff_gaussian_charFun.2 ⟨0, innerSL ℝ,
    LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ (L : (a : E) → ℝ) x) 0
have rw : Eq (α := ℝ) ((L : (a : E) → ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) : ℝ) (0 : ℝ)
Tactic: rw [L.integral_comp_id_comm IsGaussian.integrable_id, integral_id_stdGaussian, map_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
rw : Eq (α := ℝ) ((L : (a : E) → ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ (L : (a : E) → ℝ) x) 0
have rw₁ : Eq (α := ℝ) ((L : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [L.integral_comp_id_comm IsGaussian.integrable_id, integral_id_stdGaussian, map_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
rw : Eq (α := ℝ) ((L : (a : E) → ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) ((L : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ (L : (a : E) → ℝ) x) 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [L.integral_comp_id_comm IsGaussian.integrable_id, integral_id_stdGaussian, map_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (stdGaussian E)) (innerSL ℝ)
have refine_1 : LinearMap.BilinForm.IsPosSemidef.{0, u_2} (M := E) (ContinuousLinearMap.toBilinForm (innerSL ℝ))
Tactic: refine gaussian_charFun_congr 0 _ ?_ ?_ |>.2.symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
refine_1 : LinearMap.BilinForm.IsPosSemidef.{0, u_2} (M := E) (ContinuousLinearMap.toBilinForm (innerSL ℝ))
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (stdGaussian E)) (innerSL ℝ)
have refine_2 : ∀ (t : E),
  charFun (mE := inst_3) (stdGaussian E) t =
    cexp ((↑⟪t, 0⟫ : ℂ) * I - (↑((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
Tactic: refine gaussian_charFun_congr 0 _ ?_ ?_ |>.2.symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
⊢ Eq (α := Measure F) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) (stdGaussian F)
have this : FiniteDimensional ℝ F
Tactic: have := f.finiteDimensional
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
⊢ Eq (α := Measure F) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) (stdGaussian F)
have h : Eq (α := (L : StrongDual ℝ F) → ℂ) (charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)))
  (charFunDual (mE := inst_7) (stdGaussian F))
Tactic: apply Measure.ext_of_charFunDual
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
⊢ Eq (α := (L : StrongDual ℝ F) → ℂ) (charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)))
    (charFunDual (mE := inst_7) (stdGaussian F))
have h : ∀ (L : StrongDual ℝ F),
  charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
Tactic: ext L
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
⊢ charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
have h : charFunDual (mE := inst_7) (Measure.map (⇑f.toLinearIsometry.toContinuousLinearMap : (a : E) → F) (stdGaussian E)) L =
  charFunDual (mE := inst_7) (stdGaussian F) L
Tactic: simp_rw [show ⇑f = f.toLinearIsometry.toContinuousLinearMap from rfl, charFunDual_map,
    charFunDual_stdGaussian, L.opNorm_comp_linearIsometryEquiv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
h :
  charFunDual (mE := inst_7) (Measure.map (⇑f.toLinearIsometry.toContinuousLinearMap : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
⊢ charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
have h₁ : charFunDual (mE := inst_3) (stdGaussian E) (L ∘SL f.toLinearIsometry.toContinuousLinearMap) =
  charFunDual (mE := inst_7) (stdGaussian F) L
Tactic: simp_rw [show ⇑f = f.toLinearIsometry.toContinuousLinearMap from rfl, charFunDual_map,
    charFunDual_stdGaussian, L.opNorm_comp_linearIsometryEquiv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
h :
  charFunDual (mE := inst_7) (Measure.map (⇑f.toLinearIsometry.toContinuousLinearMap : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
h₁ :
  charFunDual (mE := inst_3) (stdGaussian E) (L ∘SL f.toLinearIsometry.toContinuousLinearMap) =
    charFunDual (mE := inst_7) (stdGaussian F) L
⊢ charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) L =
    charFunDual (mE := inst_7) (stdGaussian F) L
have h₂ : cexp (-HPow.hPow (β := ℕ) (↑‖L ∘SL f.toLinearIsometry.toContinuousLinearMap‖ : ℂ) 2 / 2) =
  cexp (-HPow.hPow (β := ℕ) (↑‖L‖ : ℂ) 2 / 2)
Tactic: simp_rw [show ⇑f = f.toLinearIsometry.toContinuousLinearMap from rfl, charFunDual_map,
    charFunDual_stdGaussian, L.opNorm_comp_linearIsometryEquiv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Eq.{u_1 + 1} (α := Measure (WithLp 2 ((i : ι) → ℝ)))
    (Measure.map (toLp 2) (Measure.pi (α := fun (x : ι) ↦ ℝ) fun (x : ι) ↦ gaussianReal 0 1))
    (stdGaussian (EuclideanSpace ℝ ι))
have 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 ℝ ι)))
Tactic: apply Measure.ext_of_charFun (E := EuclideanSpace ℝ ι)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ 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 ℝ ι)))
have 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
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_1
inst : Fintype ι
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
have 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)
Tactic: simp_rw [charFun_stdGaussian, charFun_pi, charFun_gaussianReal, ← exp_sum, ← ofReal_pow,
    EuclideanSpace.real_norm_sq_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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))
have 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))
Tactic: simp_rw [← b.equiv_apply_euclideanSpace]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
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 (α := 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))
have 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))
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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))
⊢ 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))
have hg : Measurable.{u_1, u_2} (α := EuclideanSpace ℝ ι) (β := E)
  (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
Tactic: rw [this, ← Measure.map_map, map_pi_eq_stdGaussian, stdGaussian_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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)
⊢ 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))
have hf : Measurable.{u_1, u_1} (α := (i : ι) → ℝ) (β := EuclideanSpace ℝ ι) (toLp 2)
Tactic: rw [this, ← Measure.map_map, map_pi_eq_stdGaussian, stdGaussian_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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_2} (α := EuclideanSpace ℝ ι) (β := E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
have funProp : LE.le.{u_1} (α := MeasurableSpace (EuclideanSpace ℝ ι)) (WithLp.measurableSpace 2 ((i : ι) → (fun (x : ι) ↦ ℝ) i))
  (WithLp.measurableSpace 2 ((i : ι) → ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
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 : ι) → ℝ))
⊢ Measurable.{u_1, u_2} (α := EuclideanSpace ℝ ι) (β := E)
    (⇑(OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι)) : (a : EuclideanSpace ℝ ι) → E)
have funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := E) fun (a : EuclideanSpace ℝ ι) ↦
  (OrthonormalBasis.equiv (EuclideanSpace.basisFun ι ℝ) b (Equiv.refl ι) : (a : EuclideanSpace ℝ ι) → E) a
Tactic: 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 ι ι ℝ
hS : ¬S.PosSemidef
⊢ multivariateGaussian μ S = Measure.dirac μ
have 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 μ)
Tactic: rw [multivariateGaussian, CFC.sqrt, cfcₙ_apply_of_not_predicate]
-- 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
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 μ)
⊢ multivariateGaussian μ S = Measure.dirac μ
have ha : ¬0 ≤ S
Tactic: rw [multivariateGaussian, CFC.sqrt, cfcₙ_apply_of_not_predicate]