awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₂ : ‖L₂‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
⊢ ‖L₂‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y : StrongDual ℝ (E × F)
⊢ (((L₁.diagonalStrongDualProd L₂ : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ) x :
          StrongDual ℝ (E × F) →L[ℝ] ℝ) :
        (a : StrongDual ℝ (E × F)) → ℝ)
      y =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y : StrongDual ℝ (E × F)
⊢ ((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
          StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ (E × F)) → ℝ)
      y =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x y : StrongDual ℝ (E × F)
simp_rw :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (y ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (x ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (y ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)
simp_rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (y ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)
⊢ Eq (α := ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        y :
      ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) y :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        x :
      ℝ)

Tactic:
simp_rw [toBilinForm_diagonalStrongDualProd_apply, h₁.eq, h₂.eq]

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsPosSemidef.isSymm, _private.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualProd_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
rw :
  0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (x ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        x :
      ℝ)

Tactic:
rw [toBilinForm_diagonalStrongDualProd_apply]

Premises used: _private.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualProd_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (x ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)

Tactic:
add_nonneg (h₁.nonneg _) (h₂.nonneg _)

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg, add_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (x ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)

Tactic:
exact add_nonneg (h₁.nonneg _) (h₂.nonneg _)

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg, add_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
⊢ IsProbabilityMeasure P

Tactic:
have := hX2.isProbabilityMeasure
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
rw :
  ∃ (m : (x : ι) → E x) (f : StrongDual ℝ ((x : ι) → E x) →L[ℝ] StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
          cexp
            ((↑((L : (a : (x : ι) → E x) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) L :
                          StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                      L) :
                  ℂ) /
                2)
⊢ IsGaussian (E := (x : ι) → E x) (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P)

Tactic:
rw [isGaussian_iff_gaussian_charFunDual]

Premises used: ProbabilityTheory.isGaussian_iff_gaussian_charFunDual
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ (m : (x : ι) → E x) (f : StrongDual ℝ ((x : ι) → E x) →L[ℝ] StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
          cexp
            ((↑((L : (a : (x : ι) → E x) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) L :
                          StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                      L) :
                  ℂ) /
                2)

Tactic:
⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩

Premises used: ProbabilityTheory.covarianceBilinDual, ProbabilityTheory.isPosSemidef_covarianceBilinDual, MeasureTheory.integral, MeasureTheory.Measure.map, And.intro, Exists.intro, _private.0.ContinuousLinearMap.diagonalStrongDualPi, _private.0.ContinuousLinearMap.isPosSemidef_diagonalStrongDualPi
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
refine :
  ∀ (L : StrongDual ℝ ((x : ι) → E x)),
    charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
      cexp
        ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                  @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
              ℂ) *
            I -
          (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                          (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                  L) :
              ℂ) /
            2)
⊢ ∃ (m : (x : ι) → E x) (f : StrongDual ℝ ((x : ι) → E x) →L[ℝ] StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
          cexp
            ((↑((L : (a : (x : ι) → E x) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) L :
                          StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                      L) :
                  ℂ) /
                2)

Tactic:
refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
funProp : ∀ (i : ι), AEFinStronglyMeasurable.{u_1, u_3} (β := E i) (fun (a : Ω) ↦ X i a) P
⊢ ∀ (i : ι), AEMeasurable (X i) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
rw :
  ∏ i : ι,
      charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)
⊢ charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)

Tactic:
rw [(iIndepFun_iff_charFunDual_pi (by fun_prop)).1 hX2]

Premises used: ProbabilityTheory.iIndepFun_iff_charFunDual_pi, Iff.mp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
simp :
  Eq (α := ℂ)
    (∏ i : ι,
      charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)))
    (∏ x : ι,
      cexp
        ((↑((L : (a : (x : ι) → E x) → ℝ)
                  (Pi.single (M := E) x (@integral _ _ _ _ (inst_2 x) (Measure.map (X x) P) fun (x : E x) ↦ x))) :
              ℂ) *
            I -
          (↑((((covarianceBilinDual (mE := inst_2 x) (Measure.map (X x) P) :
                          (a : StrongDual ℝ (E x)) → StrongDual ℝ (E x) →L[ℝ] ℝ)
                        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x)) :
                      StrongDual ℝ (E x) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E x)) → ℝ)
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x))) :
              ℂ) /
            2))
⊢ ∏ i : ι,
      charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)

Tactic:
simp only [← LinearMap.sum_single_apply E (fun i ↦ ∫ x, x ∂P.map (X i)), map_sum, ofReal_sum,
      sum_mul, diagonalStrongDualPi_apply, sum_div, ← sum_sub_distrib, exp_sum]

Premises used: map_sum, Complex.ofReal_sum, Finset.sum_div, Finset.sum_sub_distrib, LinearMap.sum_single_apply, MeasureTheory.integral, MeasureTheory.Measure.map, Complex.exp_sum, _private.0.ContinuousLinearMap.diagonalStrongDualPi_apply, Finset.sum_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
E : ι → Type u_3
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
inst_6 : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
e_f :
  ∀ (i : ι),
    charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) =
      cexp
        ((↑((L : (a : (x : ι) → E x) → ℝ)
                  (Pi.single (M := E) i (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x))) :
              ℂ) *
            I -
          (↑((((covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                          (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) :
                      StrongDual ℝ (E i) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E i)) → ℝ)
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))) :
              ℂ) /
            2)
⊢ Eq (α := ℂ)
    (∏ i : ι,
      charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)))
    (∏ x : ι,
      cexp
        ((↑((L : (a : (x : ι) → E x) → ℝ)
                  (Pi.single (M := E) x (@integral _ _ _ _ (inst_2 x) (Measure.map (X x) P) fun (x : E x) ↦ x))) :
              ℂ) *
            I -
          (↑((((covarianceBilinDual (mE := inst_2 x) (Measure.map (X x) P) :
                          (a : StrongDual ℝ (E x)) → StrongDual ℝ (E x) →L[ℝ] ℝ)
                        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x)) :
                      StrongDual ℝ (E x) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E x)) → ℝ)
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x))) :
              ℂ) /
            2))

Tactic:
congr with i