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 ι
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 ω) : ℝ)
⊢ (↑(∫ (ω : Ω), ∑ 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) : ℂ)
have 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) : ℂ)
Tactic: rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]
-- 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 ι
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 ω) : ℝ)
⊢ (↑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
have 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
Tactic: rw [variance_fun_sum fun i ↦ ((hX.eval i).map_fun _).memLp_two]
-- 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 ι
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 ω) : ℝ)
⊢ (↑(∑ 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
have 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])
Tactic: simp only [← sum_div, ← ofReal_sum, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      div_left_inj', ofReal_inj]
-- 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 ι
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 ω) : ℝ)
⊢ 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])
have 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] =
    Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
Tactic: congr with i
-- 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 ι
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 ω) : ℝ)
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] =
    Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
have e_z : cov[fun (x : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦
    (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i x); P] =
  Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
Tactic: rw [sum_eq_single_of_mem i (by grind) (fun j _ hij ↦ h i j hij.symm _ _),
      covariance_self ((hX.eval i).map_fun _).aemeasurable]
-- 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 ι
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 ω) : ℝ)
i : ι
e_z :
  cov[fun (x : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i x), fun (x : Ω) ↦
      (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i x); P] =
    Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
⊢ ∑ 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] =
    Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
have e_z₁ : Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P] =
  Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
Tactic: rw [sum_eq_single_of_mem i (by grind) (fun j _ hij ↦ h i j hij.symm _ _),
      covariance_self ((hX.eval i).map_fun _).aemeasurable]
-- 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 ι
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 : IsProbabilityMeasure P
let let₁ let₂ : iIndepFun (β := E) X P
⊢ iIndepFun (β := E) X P
have let₃ : let this := Fintype.ofFinite ι;
∀ (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))
Tactic: classical
  let := Fintype.ofFinite ι
  rw [iIndepFun_iff_charFunDual_pi fun i ↦ hX.aemeasurable.eval i]
  intro L
  have this ω : L (X · ω) = ∑ i, (L ∘L (single ℝ E i)) (X i ω) := by
    simp [← map_sum, LinearMap.sum_single_apply]
  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]
  congr
  · simp_rw [← Complex.ofReal_sum]
    rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]
  · rw [variance_fun_sum fun i ↦ ((hX.eval i).map_fun _).memLp_two]
    simp only [← sum_div, ← ofReal_sum, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      div_left_inj', ofReal_inj]
    congr with i
    rw [sum_eq_single_of_mem i (by grind) (fun j _ hij ↦ h i j hij.symm _ _),
      covariance_self ((hX.eval i).map_fun _).aemeasurable]
-- 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 ι
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 : IsProbabilityMeasure P
let let₁ let₂ : iIndepFun (β := E) X P
let₃ let₄ :
  let this := Fintype.ofFinite ι;
  ∀ (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
have let₅ : let this := Fintype.ofFinite ι;
∀ (L : StrongDual ℝ ((x : ι) → E x))
  (this_1 :
    ∀ (ω : Ω),
      Eq (α := ℝ) ((L : (a : (x : ι) → E x) → ℝ) fun (x : ι) ↦ X x ω : ℝ)
        (∑ i : ι, (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω) : ℝ)),
  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: classical
  let := Fintype.ofFinite ι
  rw [iIndepFun_iff_charFunDual_pi fun i ↦ hX.aemeasurable.eval i]
  intro L
  have this ω : L (X · ω) = ∑ i, (L ∘L (single ℝ E i)) (X i ω) := by
    simp [← map_sum, LinearMap.sum_single_apply]
  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]
  congr
  · simp_rw [← Complex.ofReal_sum]
    rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]
  · rw [variance_fun_sum fun i ↦ ((hX.eval i).map_fun _).memLp_two]
    simp only [← sum_div, ← ofReal_sum, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      div_left_inj', ofReal_inj]
    congr with i
    rw [sum_eq_single_of_mem i (by grind) (fun j _ hij ↦ h i j hij.symm _ _),
      covariance_self ((hX.eval i).map_fun _).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) 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 Ω
ι : 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 : IsProbabilityMeasure P
⊢ 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 ω)
have h₁ : ∀ (x : ι) (x_1 : Ω) (x_2 : κ x),
  X x x_2 x_1 = Function.comp (β := WithLp 2 ((j : κ x) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ x) ↦ X x j ω) x_1 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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 : IsProbabilityMeasure P
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) P
have this₁ : 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 ω)
Tactic: have : (fun i ω j ↦ X i j ω) = fun i ↦ (ofLp ∘ (toLp 2 ∘ fun ω j ↦ X i j ω)) := by ext; simp
-- 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 :
  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 ω)
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) P
have rw : iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ)
  (fun (i : ι) ↦ Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)) P
Tactic: rw [this]
-- 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 ι
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ)
    (fun (i : ι) ↦ Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)) P
have refine_1 : HasGaussianLaw (E := (i : ι) → WithLp 2 ((j : κ i) → ℝ))
  (fun (ω : Ω) (i : ι) ↦ (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω) P
Tactic: refine (HasGaussianLaw.iIndepFun_of_covariance_inner ?_ fun i j hij x y ↦ ?_).comp _ (by fun_prop)
-- 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 ι
refine_1 :
  HasGaussianLaw (E := (i : ι) → WithLp 2 ((j : κ i) → ℝ))
    (fun (ω : Ω) (i : ι) ↦ (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω) P
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ)
    (fun (i : ι) ↦ Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)) P
have refine_2 : ∀ (i j : ι) (hij : i ≠ j) (x : WithLp 2 ((j : κ i) → ℝ)) (y : WithLp 2 ((j : κ j) → ℝ)),
  cov[fun (ω : Ω) ↦ ⟪x, (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω⟫, fun (ω : Ω) ↦
      ⟪y, (toLp 2 ∘ fun (ω : Ω) (j_1 : κ j) ↦ X j j_1 ω) ω⟫; P] =
    0
Tactic: refine (HasGaussianLaw.iIndepFun_of_covariance_inner ?_ fun i j hij x y ↦ ?_).comp _ (by fun_prop)
-- 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) → ℝ)
⊢ cov[fun (ω : Ω) ↦ ⟪x, (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω⟫, fun (ω : Ω) ↦
      ⟪y, (toLp 2 ∘ fun (ω : Ω) (j_1 : κ j) ↦ X j j_1 ω) ω⟫; P] =
    0
have refine_2 : cov[fun (ω : Ω) ↦
    inner.{0, u_4} ℝ (E := WithLp 2 ((j : κ i) → ℝ))
      (∑ i_1 : κ i,
        HSMul.hSMul (α := (fun (x : κ i) ↦ ℝ) i_1) (β := EuclideanSpace ℝ (κ i))
          (ofLp (p := 2)
            ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ i) ℝ) :
                (a : EuclideanSpace ℝ (κ i)) → EuclideanSpace ℝ (κ i))
              x)
            i_1)
          ((EuclideanSpace.basisFun (κ i) ℝ : (a : κ i) → EuclideanSpace ℝ (κ i)) i_1 : EuclideanSpace ℝ (κ i)))
      ((toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω),
    fun (ω : Ω) ↦
    inner.{0, u_4} ℝ (E := WithLp 2 ((j : κ j) → ℝ))
      (∑ i : κ j,
        HSMul.hSMul (α := (fun (x : κ j) ↦ ℝ) i) (β := EuclideanSpace ℝ (κ j))
          (ofLp (p := 2)
            ((OrthonormalBasis.repr (EuclideanSpace.basisFun (κ j) ℝ) :
                (a : EuclideanSpace ℝ (κ j)) → EuclideanSpace ℝ (κ j))
              y)
            i)
          ((EuclideanSpace.basisFun (κ j) ℝ : (a : κ j) → EuclideanSpace ℝ (κ j)) i : EuclideanSpace ℝ (κ j)))
      ((toLp 2 ∘ fun (ω : Ω) (j_1 : κ j) ↦ X j j_1 ω) ω);
    P] =
  0
Tactic: rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]