awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have have : Eq.{u_2 + 1} (α := Ω → ℝ)
  (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
  (∑ i : ↥I,
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
        (a : E) → ℝ) ∘
      X (↑i : S))
Tactic: classical
  have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
  · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
  · exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
have :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have refine_2 : ∀
  (h1 :
    Eq.{u_2 + 1} (α := Ω → ℝ)
      (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
      (∑ i : ↥I,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
            (a : E) → ℝ) ∘
          X (↑i : S))),
  cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
Tactic: classical
  have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
  · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
  · exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two
-- 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) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) 0
have rw : Eq.{u_2 + 1} (α := E)
  (∑ i : Fin (finrank ℝ E),
    @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 (a : (i : Fin (finrank ℝ E)) → ℝ) ↦
      HSMul.hSMul (β := E) (a i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
  0
Tactic: rw [stdGaussian, integral_map _ (by fun_prop), integral_finsetSum]
-- 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
rw :
  Eq.{u_2 + 1} (α := E)
    (∑ i : Fin (finrank ℝ E),
      @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 (a : (i : Fin (finrank ℝ E)) → ℝ) ↦
        HSMul.hSMul (β := E) (a i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    0
⊢ Eq (α := E) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) 0
have hf : ∀ (i : Fin (finrank ℝ E)),
  Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
    @Integrable.{u_2, 0} E _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
      (fun (x : (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)
Tactic: rw [stdGaussian, integral_map _ (by fun_prop), integral_finsetSum]
-- 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
rw :
  Eq.{u_2 + 1} (α := E)
    (∑ i : Fin (finrank ℝ E),
      @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 (a : (i : Fin (finrank ℝ E)) → ℝ) ↦
        HSMul.hSMul (β := E) (a i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    0
hf :
  ∀ (i : Fin (finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
      @Integrable.{u_2, 0} E _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (fun (x : (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)
⊢ Eq (α := E) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) 0
have rw₁ : AEMeasurable.{0, u_2} (β := E) (_m := MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ 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)
Tactic: rw [stdGaussian, integral_map _ (by fun_prop), integral_finsetSum]
-- 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
⊢ variance (mΩ := inst_3) (⇑L : (a : E) → ℝ) (stdGaussian E) = HPow.hPow (β := ℕ) ‖L‖ 2
have rw : 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 [stdGaussian, variance_map L.continuous.aemeasurable (Measurable.aemeasurable (by fun_prop))]
-- 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 (α := (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))
have h : ∀ (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: ext x
-- 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
L : StrongDual ℝ E
⊢ 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
have 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))
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]
-- 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
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))
⊢ 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
have 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
Tactic: rw [this, variance_sum_pi]
-- 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
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
⊢ 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
have rw₁ : ∀ (i : Fin (finrank ℝ E)),
  MemLp (HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)) 2
    (gaussianReal 0 1)
Tactic: rw [this, variance_sum_pi]
-- 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
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),
      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
have 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)
Tactic: simp_rw [variance_const_mul, variance_id_gaussianReal, (stdOrthonormalBasis ℝ E).norm_dual]
-- 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
⊢ Measurable (β := ℂ) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)
have funProp : inst_3 ≤ inst_3
Tactic: fun_prop
-- 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
funProp : inst_3 ≤ inst_3
⊢ Measurable (β := ℂ) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E) ↦ ⟪x, t⟫
Tactic: fun_prop
-- 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
⊢ charFun (mE := inst_3) (stdGaussian E) t = cexp (-HPow.hPow (β := ℕ) (↑‖t‖ : ℂ) 2 / 2)
have 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)
Tactic: rw [charFun_apply, stdGaussian, integral_map (Measurable.aemeasurable (by fun_prop))
    (Measurable.aestronglyMeasurable (by fun_prop))]
-- 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
⊢ (@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)
have 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)
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]
-- 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
⊢ ∏ 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)
have 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)
Tactic: simp only [ofReal_zero, mul_zero, zero_mul, NNReal.coe_one, ofReal_one, one_mul,
    zero_sub]
-- 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
⊢ ∏ 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
    (∑ 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)
⊢ ∏ 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
    (-∑ 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)
⊢ ∏ 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 (α := ℂ)
        (∑ 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]