awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
x : Fin (finrank ℝ E) → ℝ
⊢ Eq (α := ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ)
      (fun (x : Fin (finrank ℝ E) → ℝ) ↦
        ∑ i : Fin (finrank ℝ E),
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
      x)
    ((∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
        HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)
          (x i))
      x)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))

Tactic:
have : L ∘ (fun x : Fin (Module.finrank ℝ E) → ℝ ↦ ∑ i, x i • stdOrthonormalBasis ℝ E i) =
      ∑ i, (fun x : Fin (Module.finrank ℝ E) → ℝ ↦ L (stdOrthonormalBasis ℝ E i) * x i) := by
    ext x; simp [mul_comm]
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
this :
  Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))
rw :
  ∑ i : Fin (finrank ℝ E),
      Var[HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ);
        gaussianReal 0 1] =
    HPow.hPow (β := ℕ) ‖L‖ 2
rw₁ :
  ∀ (i : Fin (finrank ℝ E)),
    MemLp (HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)) 2
      (gaussianReal 0 1)
⊢ variance (Ω := (i : Fin (finrank ℝ E)) → ℝ) (mΩ := MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
      (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
        ∑ i : Fin (finrank ℝ E),
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
      (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1) =
    HPow.hPow (β := ℕ) ‖L‖ 2

Tactic:
rw [this, variance_sum_pi]

Premises used: ProbabilityTheory.variance_sum_pi
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
this :
  Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))
simp_rw :
  Eq (α := ℝ)
    (∑ x : Fin (finrank ℝ E),
      HPow.hPow (α := ℝ) (β := ℕ)
          ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x : E) : ℝ) 2 *
        (↑1 : ℝ))
    (∑ i : Fin (finrank ℝ E),
      HPow.hPow (α := ℝ) (β := ℕ)
        ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) 2)
⊢ ∑ i : Fin (finrank ℝ E),
      Var[fun (x : ℝ) ↦
        HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)
          (id x);
        gaussianReal 0 1] =
    HPow.hPow (β := ℕ) ‖L‖ 2

Tactic:
simp_rw [variance_const_mul, variance_id_gaussianReal, (stdOrthonormalBasis ℝ E).norm_dual]

Premises used: Real, ProbabilityTheory.variance_id_gaussianReal, OrthonormalBasis.norm_dual, ProbabilityTheory.variance_const_mul, stdOrthonormalBasis
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
this :
  Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))
⊢ Eq (α := ℝ)
    (∑ x : Fin (finrank ℝ E),
      HPow.hPow (α := ℝ) (β := ℕ)
          ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x : E) : ℝ) 2 *
        (↑1 : ℝ))
    (∑ i : Fin (finrank ℝ E),
      HPow.hPow (α := ℝ) (β := ℕ)
        ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
this :
  Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))
⊢ ∀ (i : Fin (finrank ℝ E)),
    MemLp (HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)) 2
      (gaussianReal 0 1)

Tactic:
fun i ↦ IsGaussian.memLp_two_id.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, Real, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
this :
  Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))
⊢ ∀ (i : Fin (finrank ℝ E)),
    MemLp (HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)) 2
      (gaussianReal 0 1)

Tactic:
exact fun i ↦ IsGaussian.memLp_two_id.const_mul _

Premises used: MeasureTheory.MemLp.const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
⊢ Measurable.{0, u_2} (β := E) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
    ∑ i : Fin (finrank ℝ E), HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
funProp : inst_3 ≤ inst_3
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E) ↦ ⟪x, t⟫
⊢ Measurable (β := ℂ) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
rw :
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
      (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
      fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
      cexp
        ((↑⟪∑ i : Fin (finrank ℝ E),
                  HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E),
                t⟫ :
            ℂ) *
          I)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
⊢ charFun (mE := inst_3) (stdGaussian E) t = cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)

Tactic:
rw [charFun_apply, stdGaussian, integral_map (Measurable.aemeasurable (by fun_prop))
    (Measurable.aestronglyMeasurable (by fun_prop))]

Premises used: Measurable.aemeasurable, MeasureTheory.charFun_apply, MeasureTheory.integral_map, Measurable.aestronglyMeasurable, ProbabilityTheory.stdGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 :
  ∏ x : Fin (finrank ℝ E),
      cexp
        ((↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) * (↑0 : ℂ) * I -
          (↑(↑1 : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 /
            2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
      (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
      fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
      cexp
        ((↑⟪∑ i : Fin (finrank ℝ E),
                  HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E),
                t⟫ :
            ℂ) *
          I)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)

Tactic:
simp_rw [sum_inner, ofReal_sum, Finset.sum_mul, exp_sum,
    integral_fintype_prod_eq_prod (f := fun i x ↦ exp (⟪x • stdOrthonormalBasis ℝ E i, t⟫ * I)),
    real_inner_smul_left, mul_comm _ (⟪_, _⟫), ofReal_mul, ← charFun_apply_real,
    charFun_gaussianReal]

Premises used: Real, MeasureTheory.integral_fintype_prod_eq_prod, HMul.hMul, Inner.inner, MeasureTheory.charFun_apply_real, sum_inner, Complex.ofReal_sum, Complex.ofReal, mul_comm, Complex.exp, HSMul.hSMul, Complex.exp_sum, real_inner_smul_left, ProbabilityTheory.charFun_gaussianReal, DFunLike.coe, Complex.ofReal_mul, Finset.sum_mul, stdOrthonormalBasis, Complex.I
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 :
  ∏ x : Fin (finrank ℝ E),
      cexp (-(HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 / 2)) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
⊢ ∏ x : Fin (finrank ℝ E),
      cexp
        ((↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) * (↑0 : ℂ) * I -
          (↑(↑1 : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑⟪(stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) x, t⟫ : ℂ) 2 /
            2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)

Tactic:
simp only [ofReal_zero, mul_zero, zero_mul, NNReal.coe_one, ofReal_one, one_mul,
    zero_sub]

Premises used: MulZeroClass.zero_mul, Complex.ofReal_one, MulZeroClass.mul_zero, Complex.ofReal_zero, NNReal.coe_one, one_mul, zero_sub
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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)
simp_rw₅ : cexp (-((↑(HPow.hPow (β := ℕ) ‖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)

Tactic:
simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]

Premises used: Real, neg_div, OrthonormalBasis.sum_sq_inner_right, Complex.ofReal_sum, Finset.sum_div, Complex.exp_sum, Finset.sum_neg_distrib, Complex.ofReal_pow, stdOrthonormalBasis
-- 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
⊢ IsGaussian (mE := inst_4) (stdGaussian E)

Tactic:
isGaussian_iff_gaussian_charFun.2 ⟨0, innerSL ℝ,
    LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner, ?_⟩

Premises used: Iff.mpr, ProbabilityTheory.isGaussian_iff_gaussian_charFun, LinearMap.BilinForm.isPosSemidef_iff, Real, innerSL, And.intro, Exists.intro, OfNat.ofNat, isPosSemidef_inner
-- 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
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)
⊢ IsGaussian (mE := inst_4) (stdGaussian E)

Tactic:
refine isGaussian_iff_gaussian_charFun.2 ⟨0, innerSL ℝ,
    LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner, ?_⟩

Premises used: Iff.mpr, ProbabilityTheory.isGaussian_iff_gaussian_charFun, LinearMap.BilinForm.isPosSemidef_iff, Real, innerSL, And.intro, Exists.intro, OfNat.ofNat, isPosSemidef_inner
-- 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
⊢ ∀ (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:
simp [charFun_stdGaussian, neg_div, innerSL_apply_apply ℝ]

Premises used: Real, innerSL_apply_apply, neg_div, ProbabilityTheory.charFun_stdGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 : ℝ)
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ (L : (a : E) → ℝ) x) 0

Tactic:
rw [L.integral_comp_id_comm IsGaussian.integrable_id, integral_id_stdGaussian, map_zero]

Premises used: ProbabilityTheory.integral_id_stdGaussian, map_zero, ContinuousLinearMap.integral_comp_id_comm, ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
⊢ charFunDual (mE := inst_3) (stdGaussian E) L = cexp (-HPow.hPow (β := ℕ) (↑‖L‖ : ℂ) 2 / 2)

Tactic:
simp [IsGaussian.charFunDual_eq, integral_complex_ofReal, variance_dual_stdGaussian, neg_div]

Premises used: neg_div, ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.variance_dual_stdGaussian, integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 ℝ)

Tactic:
gaussian_charFun_congr 0 _ ?_ ?_ |>.2.symm

Premises used: ProbabilityTheory.gaussian_charFun_congr, And.right, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 ℝ))
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)
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (stdGaussian E)) (innerSL ℝ)

Tactic:
refine gaussian_charFun_congr 0 _ ?_ ?_ |>.2.symm

Premises used: ProbabilityTheory.gaussian_charFun_congr, And.right, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ LinearMap.BilinForm.IsPosSemidef.{0, u_2} (M := E) (ContinuousLinearMap.toBilinForm (innerSL ℝ))

Tactic:
LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner

Premises used: Iff.mpr, LinearMap.BilinForm.isPosSemidef_iff, isPosSemidef_inner
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ LinearMap.BilinForm.IsPosSemidef.{0, u_2} (M := E) (ContinuousLinearMap.toBilinForm (innerSL ℝ))

Tactic:
exact LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner

Premises used: Iff.mpr, LinearMap.BilinForm.isPosSemidef_iff, isPosSemidef_inner
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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),
    charFun (mE := inst_3) (stdGaussian E) t =
      cexp ((↑⟪t, 0⟫ : ℂ) * I - (↑((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)

Tactic:
simp [charFun_stdGaussian, neg_div, innerSL_apply_apply ℝ]

Premises used: Real, innerSL_apply_apply, neg_div, ProbabilityTheory.charFun_stdGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
⊢ FiniteDimensional ℝ F

Tactic:
have := f.finiteDimensional
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
h :
  Eq (α := (L : StrongDual ℝ F) → ℂ) (charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)))
    (charFunDual (mE := inst_7) (stdGaussian F))
⊢ Eq (α := Measure F) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) (stdGaussian F)

Tactic:
apply Measure.ext_of_charFunDual

Premises used: MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
h :
  ∀ (L : StrongDual ℝ F),
    charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)) L =
      charFunDual (mE := inst_7) (stdGaussian F) L
⊢ Eq (α := (L : StrongDual ℝ F) → ℂ) (charFunDual (mE := inst_7) (Measure.map (⇑f : (a : E) → F) (stdGaussian E)))
    (charFunDual (mE := inst_7) (stdGaussian F))

Tactic:
ext L
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
h₂ :
  cexp (-HPow.hPow (β := ℕ) (↑‖L ∘SL f.toLinearIsometry.toContinuousLinearMap‖ : ℂ) 2 / 2) =
    cexp (-HPow.hPow (β := ℕ) (↑‖L‖ : ℂ) 2 / 2)
⊢ charFunDual (mE := inst_7) (Measure.map (⇑f : (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]

Premises used: ContinuousLinearMap.opNorm_comp_linearIsometryEquiv, MeasureTheory.charFunDual_map, rfl, ProbabilityTheory.charFunDual_stdGaussian