awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
κ : ι → Type u_4
inst_1 : ∀ (i : ι), Finite.{u_4 + 1} (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (E := (i : ι) → (j : κ i) → ℝ) (fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this_1 : IsProbabilityMeasure P
this_2 :
  Eq (α := (i : ι) → (ω : Ω) → (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) fun (i : ι) ↦
    Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)
this_3 : (i : ι) → Fintype (κ i) := fun (i : ι) ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 ((j : κ i) → ℝ)
y : WithLp 2 ((j : κ j) → ℝ)
⊢ ∀ (i_1 : κ i),
    MemLp (ε := ℝ)
      (fun (ω : Ω) ↦
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ i) ℝ) :
                    (a : EuclideanSpace ℝ (κ i)) → EuclideanSpace ℝ (κ i))
                  x)
                i_1) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((j : κ i) → ℝ))
            ((EuclideanSpace.basisFun (κ i) ℝ : (a : κ i) → EuclideanSpace ℝ (κ i)) i_1 : EuclideanSpace ℝ (κ i))
            ((toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω : WithLp 2 ((j : κ i) → ℝ))))
      2 P

Tactic:
simpa using fun j ↦ ((hX.eval i).eval j).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.eval, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
κ : ι → Type u_4
inst_1 : ∀ (i : ι), Finite.{u_4 + 1} (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (E := (i : ι) → (j : κ i) → ℝ) (fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this_1 : IsProbabilityMeasure P
this_2 :
  Eq (α := (i : ι) → (ω : Ω) → (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) fun (i : ι) ↦
    Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)
this_3 : (i : ι) → Fintype (κ i) := fun (i : ι) ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 ((j : κ i) → ℝ)
y : WithLp 2 ((j : κ j) → ℝ)
⊢ ∀ (i : κ j),
    MemLp (ε := ℝ)
      (fun (ω : Ω) ↦
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ j) ℝ) :
                    (a : EuclideanSpace ℝ (κ j)) → EuclideanSpace ℝ (κ j))
                  y)
                i) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((j : κ j) → ℝ))
            ((EuclideanSpace.basisFun (κ j) ℝ : (a : κ j) → EuclideanSpace ℝ (κ j)) i : EuclideanSpace ℝ (κ j))
            ((toLp 2 ∘ fun (ω : Ω) (j_1 : κ j) ↦ X j j_1 ω) ω : WithLp 2 ((j : κ j) → ℝ))))
      2 P

Tactic:
simpa using fun i ↦ ((hX.eval j).eval i).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.eval, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
X : ι → Ω → ℝ
hX : HasGaussianLaw.{u_1, u_2} (E := ι → ℝ) (fun (ω : Ω) (x : ι) ↦ X x ω) P
h : ∀ (i j : ι), i ≠ j → cov[X i, X j; P] = 0
i j : ι
hij : i ≠ j
L₁ L₂ : StrongDual ℝ ℝ
⊢ cov[(⇑L₁ : (a : ℝ) → ℝ) ∘ X i, (⇑L₂ : (a : ℝ) → ℝ) ∘ X j; P] = 0

Tactic:
simp [Function.comp_def, ← toDual_symm_apply, covariance_mul_const_right,
      covariance_mul_const_left, h, hij]

Premises used: InnerProductSpace.toDual_symm_apply, ProbabilityTheory.covariance_mul_const_left, Function.comp_def, ProbabilityTheory.covariance_mul_const_right
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
⊢ IsProbabilityMeasure P

Tactic:
have := hX.isProbabilityMeasure
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
rw :
  ∃ (m : E × F) (f : StrongDual ℝ (E × F) →L[ℝ] StrongDual ℝ (E × F) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
          cexp
            ((↑((L : (a : E × F) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ) L : StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ (E × F)) → ℝ)
                      L) :
                  ℂ) /
                2)
⊢ IsGaussian (E := E × F) (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) 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 Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
⊢ ∃ (m : E × F) (f : StrongDual ℝ (E × F) →L[ℝ] StrongDual ℝ (E × F) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
          cexp
            ((↑((L : (a : E × F) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ) L : StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ (E × F)) → ℝ)
                      L) :
                  ℂ) /
                2)

Tactic:
⟨(∫ x, x ∂P.map X, ∫ y, y ∂P.map Y),
      .diagonalStrongDualProd (covarianceBilinDual (P.map X)) (covarianceBilinDual (P.map Y)),
      isPosSemidef_diagonalStrongDualProd isPosSemidef_covarianceBilinDual
        isPosSemidef_covarianceBilinDual, fun L ↦ ?_⟩

Premises used: Prod.mk, ProbabilityTheory.covarianceBilinDual, _private.0.ContinuousLinearMap.isPosSemidef_diagonalStrongDualProd, ProbabilityTheory.isPosSemidef_covarianceBilinDual, MeasureTheory.integral, MeasureTheory.Measure.map, And.intro, Exists.intro, _private.0.ContinuousLinearMap.diagonalStrongDualProd
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
refine :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      cexp
        ((↑((L : (a : E × F) → ℝ)
                  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                    @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
              ℂ) *
            I -
          (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                            (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                          (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E × F)) → ℝ)
                  L) :
              ℂ) /
            2)
⊢ ∃ (m : E × F) (f : StrongDual ℝ (E × F) →L[ℝ] StrongDual ℝ (E × F) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
          cexp
            ((↑((L : (a : E × F) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ) L : StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ (E × F)) → ℝ)
                      L) :
                  ℂ) /
                2)

Tactic:
refine ⟨(∫ x, x ∂P.map X, ∫ y, y ∂P.map Y),
      .diagonalStrongDualProd (covarianceBilinDual (P.map X)) (covarianceBilinDual (P.map Y)),
      isPosSemidef_diagonalStrongDualProd isPosSemidef_covarianceBilinDual
        isPosSemidef_covarianceBilinDual, fun L ↦ ?_⟩
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
⊢ AEMeasurable X P

Tactic:
fun_prop
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
funProp : AEFinStronglyMeasurable.{u_1, u_3} (β := F) (fun (a : Ω) ↦ Y a) P
⊢ AEMeasurable Y P

Tactic:
fun_prop
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
rw :
  charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                  @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                          (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                        (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E × F)) → ℝ)
                L) :
            ℂ) /
          2)
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                  @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                          (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                        (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E × F)) → ℝ)
                L) :
            ℂ) /
          2)

Tactic:
rw [(indepFun_iff_charFunDual_prod (by fun_prop) (by fun_prop)).1 hXY]

Premises used: Iff.mp, ProbabilityTheory.indepFun_iff_charFunDual_prod
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)

Tactic:
simp
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)

Tactic:
have : (∫ x, x ∂Measure.map X P, ∫ y, y ∂Measure.map Y P) =
        ContinuousLinearMap.inl ℝ E F (∫ x, x ∂Measure.map X P) +
        ContinuousLinearMap.inr ℝ E F (∫ y, y ∂Measure.map Y P) := by simp
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
e_a :
  cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F) : (a : E) → ℝ)
                (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_1) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ)
                (Measure.map X P)) :
            ℂ) /
          2) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_1) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ)
                (Measure.map X P)) :
            ℂ) /
          2)
e_a₁ : MemLp (m0 := inst_1) id 2 (Measure.map X P)
e_a₂ : @Integrable _ _ _ _ inst_1 id (Measure.map X P)
⊢ charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)) :
            ℂ) *
          I -
        (↑((((covarianceBilinDual (mE := inst_1) (Measure.map X P) : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
                      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) :
                    StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F))) :
            ℂ) /
          2)

Tactic:
rw [hX.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.covarianceBilinDual_self_eq_variance, integral_complex_ofReal, ContinuousLinearMap.integral_comp_id_comm
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F) : (a : E) → ℝ)
                (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_1) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ)
                (Measure.map X P)) :
            ℂ) /
          2) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_1) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ)
                (Measure.map X P)) :
            ℂ) /
          2)

Tactic:
simp
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ MemLp (m0 := inst_1) id 2 (Measure.map X P)

Tactic:
hX.isGaussian_map.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- 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 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ MemLp (m0 := inst_1) id 2 (Measure.map X P)

Tactic:
exact hX.isGaussian_map.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id