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 ι
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)
i : ι
e_f :
  cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ)
                (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_2 i)
                (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                (Measure.map (X i) P)) :
            ℂ) /
          2) =
    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 -
        (↑(variance (mΩ := inst_2 i)
                (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                (Measure.map (X i) P)) :
            ℂ) /
          2)
e_f₁ : MemLp (m0 := inst_2 i) id 2 (Measure.map (X i) P)
e_f₂ : @Integrable _ _ _ _ (inst_2 i) id (Measure.map (X i) P)
⊢ 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)

Tactic:
rw [(hX1 i).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 Ω
ι : 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)
i : ι
⊢ cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ)
                (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_2 i)
                (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                (Measure.map (X i) P)) :
            ℂ) /
          2) =
    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 -
        (↑(variance (mΩ := inst_2 i)
                (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                (Measure.map (X i) P)) :
            ℂ) /
          2)

Tactic:
simp
-- 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)
i : ι
⊢ MemLp (m0 := inst_2 i) id 2 (Measure.map (X i) P)

Tactic:
(hX1 i).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 Ω
ι : 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)
i : ι
⊢ MemLp (m0 := inst_2 i) id 2 (Measure.map (X i) P)

Tactic:
exact (hX1 i).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 Ω
ι : 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)
i : ι
⊢ @Integrable _ _ _ _ (inst_2 i) id (Measure.map (X i) P)

Tactic:
(hX1 i).isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- 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)
i : ι
⊢ @Integrable _ _ _ _ (inst_2 i) id (Measure.map (X i) P)

Tactic:
exact (hX1 i).isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
⊢ IsProbabilityMeasure P

Tactic:
have := hX.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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
rw :
  ∀ (L : StrongDual ℝ ((x : ι) → E x)),
    charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
      ∏ i : ι,
        charFunDual.{u_3} (E := E i) (mE := inst_2 i) (Measure.map (fun (x : Ω) ↦ X i x) P)
          (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))
⊢ iIndepFun (β := E) X P

Tactic:
rw [iIndepFun_iff_charFunDual_pi fun i ↦ hX.aemeasurable.eval i]

Premises used: ProbabilityTheory.iIndepFun_iff_charFunDual_pi, AEMeasurable.eval, ProbabilityTheory.HasGaussianLaw.aemeasurable
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
ω : Ω
⊢ Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
    (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)

Tactic:
simp [← map_sum, LinearMap.sum_single_apply]

Premises used: map_sum, LinearMap.sum_single_apply
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
⊢ ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)

Tactic:
have this ω : L (X · ω) = ∑ i, (L ∘L (single ℝ E i)) (X i ω) := by
    simp [← map_sum, LinearMap.sum_single_apply]
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
simp_rw :
  cexp
      ((↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) * I -
        (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) /
          2) =
    cexp
      ((∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)) * I -
        ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2)
⊢ charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
    ∏ i : ι,
      charFunDual.{u_3} (E := E i) (mE := inst_2 i) (Measure.map (fun (x : Ω) ↦ X i x) P)
        (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))

Tactic:
simp_rw [hX.charFunDual_map_eq_fun, fun i ↦ (hX.eval i).charFunDual_map_eq_fun, ← Complex.exp_sum,
    sum_sub_distrib, ← sum_mul, this]

Premises used: Finset.sum_sub_distrib, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, Complex.exp_sum, ProbabilityTheory.HasGaussianLaw.eval, 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
e_z :
  (↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) =
    ∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)
e_z₁ :
  (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) / 2 =
    ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2
⊢ cexp
      ((↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) * I -
        (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) /
          2) =
    cexp
      ((∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)) * I -
        ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2)

Tactic:
congr
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
e_z :
  (↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) =
    (↑(∑ i : ι, ∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)
⊢ (↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) =
    ∑ i : ι, (↑(∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)

Tactic:
simp_rw [← Complex.ofReal_sum]

Premises used: Complex.ofReal_sum
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
e_z e_z₁ :
  (↑(∑ i : ι, ∫ (a : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i a) ∂P) : ℂ) =
    (↑(∑ i : ι, ∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)
⊢ (↑(∫ (ω : Ω), ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ) =
    (↑(∑ i : ι, ∫ (ω : Ω), (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) ∂P) : ℂ)

Tactic:
rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]

Premises used: MeasureTheory.integral_finsetSum
-- 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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
e_z :
  (↑(∑ i : ι,
            ∑ j : ι,
              cov[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω), fun (ω : Ω) ↦
                (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E j) : (a : E j) → ℝ) (X j ω); P]) :
        ℂ) /
      2 =
    ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2
⊢ (↑Var[fun (ω : Ω) ↦ ∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] : ℂ) / 2 =
    ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2

Tactic:
rw [variance_fun_sum fun i ↦ ((hX.eval i).map_fun _).memLp_two]

Premises used: ProbabilityTheory.variance_fun_sum, ProbabilityTheory.HasGaussianLaw.map_fun, 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 ι
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
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j →
      ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
        cov[fun (x : Ω) ↦ (L₁ : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦ (L₂ : (a : E j) → ℝ) (X j x); P] = 0
this_1 : IsProbabilityMeasure P
this_2 : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this :
  ∀ (ω : Ω),
    Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
      (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)
e_z :
  Eq (α := ℝ)
    (∑ i : ι,
      ∑ j : ι,
        cov[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω), fun (ω : Ω) ↦
          (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E j) : (a : E j) → ℝ) (X j ω); P])
    (∑ i : ι, Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P])
⊢ (↑(∑ i : ι,
            ∑ j : ι,
              cov[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω), fun (ω : Ω) ↦
                (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E j) : (a : E j) → ℝ) (X j ω); P]) :
        ℂ) /
      2 =
    ∑ x : ι, (↑Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x) : (a : E x) → ℝ) (X x ω); P] : ℂ) / 2

Tactic:
simp only [← sum_div, ← ofReal_sum, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      div_left_inj', ofReal_inj]

Premises used: OfNat.ofNat_ne_zero, Complex.ofReal_sum, ne_eq, Finset.sum_div, Complex.ofReal_inj, div_left_inj', not_false_eq_true