awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
⊢ Eq (α := ℝ)
    (∑ i_1 : κ i,
      ∑ j_1 : κ j,
        cov[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) → ℝ))),
          fun (ω : Ω) ↦
          HMul.hMul (α := ℝ)
            ((starRingEnd ℝ : (a : ℝ) → ℝ)
                (ofLp (p := 2)
                  ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ j) ℝ) :
                      (a : EuclideanSpace ℝ (κ j)) → EuclideanSpace ℝ (κ j))
                    y)
                  j_1) :
              ℝ)
            (inner ℝ (E := WithLp 2 ((j : κ j) → ℝ))
              ((EuclideanSpace.basisFun (κ j) ℝ : (a : κ j) → EuclideanSpace ℝ (κ j)) j_1 : EuclideanSpace ℝ (κ j))
              ((toLp 2 ∘ fun (ω : Ω) (j_2 : κ j) ↦ X j j_2 ω) ω : WithLp 2 ((j : κ j) → ℝ)));
          P])
    0
have refine_2 : Eq (α := ℝ)
  (∑ x_1 : κ i, ∑ x_2 : κ j, cov[fun (ω : Ω) ↦ x.ofLp x_1 * X i x_1 ω, fun (ω : Ω) ↦ y.ofLp x_2 * X j x_2 ω; P]) 0
Tactic: simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
⊢ Eq (α := ℝ)
    (∑ x_1 : κ i, ∑ x_2 : κ j, cov[fun (ω : Ω) ↦ x.ofLp x_1 * X i x_1 ω, fun (ω : Ω) ↦ y.ofLp x_2 * X j x_2 ω; P]) 0
have refine_2 : ∀ (k : κ i),
  Membership.mem (γ := Finset (κ i)) univ k →
    ∀ (l : κ j),
      Membership.mem (γ := Finset (κ j)) univ l →
        cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
Tactic: refine sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
k : κ i
h_1 : Membership.mem (γ := Finset (κ i)) univ k
l : κ j
h_2 : Membership.mem (γ := Finset (κ j)) univ l
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
have refine_2 : x.ofLp k * cov[X i k, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
k : κ i
h_1 : Membership.mem (γ := Finset (κ i)) univ k
l : κ j
h_2 : Membership.mem (γ := Finset (κ j)) univ l
refine_2 : x.ofLp k * cov[X i k, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
have refine_2₁ : x.ofLp k * (y.ofLp l * cov[X i k, X j l; P]) = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
k : κ i
h_1 : Membership.mem (γ := Finset (κ i)) univ k
l : κ j
h_2 : Membership.mem (γ := Finset (κ j)) univ l
refine_2 : x.ofLp k * cov[X i k, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
refine_2₁ : x.ofLp k * (y.ofLp l * cov[X i k, X j l; P]) = 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
have refine_2₂ : x.ofLp k * (y.ofLp l * 0) = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
k : κ i
h_1 : Membership.mem (γ := Finset (κ i)) univ k
l : κ j
h_2 : Membership.mem (γ := Finset (κ j)) univ l
refine_2 : x.ofLp k * cov[X i k, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
refine_2₁ : x.ofLp k * (y.ofLp l * cov[X i k, X j l; P]) = 0
refine_2₂ : x.ofLp k * (y.ofLp l * 0) = 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
have refine_2₃ : x.ofLp k * 0 = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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) → ℝ)
k : κ i
h_1 : Membership.mem (γ := Finset (κ i)) univ k
l : κ j
h_2 : Membership.mem (γ := Finset (κ j)) univ l
refine_2 : x.ofLp k * cov[X i k, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
refine_2₁ : x.ofLp k * (y.ofLp l * cov[X i k, X j l; P]) = 0
refine_2₂ : x.ofLp k * (y.ofLp l * 0) = 0
refine_2₃ : x.ofLp k * 0 = 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X i k ω, fun (ω : Ω) ↦ y.ofLp l * X j l ω; P] = 0
have refine_2₄ : Eq (α := ℝ) 0 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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
⊢ IsGaussian (E := E × F) (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
have this : IsProbabilityMeasure P
Tactic: have := hX.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ IsGaussian (E := E × F) (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
have 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)
Tactic: rw [isGaussian_iff_gaussian_charFunDual]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
have 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)
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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
⊢ AEMeasurable X P
have funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
⊢ AEMeasurable Y P
have funProp : AEFinStronglyMeasurable.{u_1, u_3} (β := F) (fun (a : Ω) ↦ Y a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
⊢ 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)
have 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)
Tactic: rw [(indepFun_iff_charFunDual_prod (by fun_prop) (by fun_prop)).1 hXY]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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)
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]