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
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] =
      Var[fun (ω : Ω) ↦ (comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ) (X i ω); P]
⊢ 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:
congr with i
-- 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 ω) : ℝ)
i : ι
⊢ Membership.mem (γ := Finset ι) univ i

Tactic:
grind
-- 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 ω) : ℝ)
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]
e_z₁ 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]
⊢ ∑ 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:
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]

Premises used: Finset.sum_eq_single_of_mem, Ne.symm, ProbabilityTheory.HasGaussianLaw.map_fun, ProbabilityTheory.HasGaussianLaw.eval, ProbabilityTheory.HasGaussianLaw.aemeasurable, ProbabilityTheory.covariance_self
-- 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 : ι) → InnerProductSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (E := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (x : E i) (y : E j), cov[fun (ω : Ω) ↦ ⟪x, X i ω⟫, fun (ω : Ω) ↦ ⟪y, X j ω⟫; P] = 0
i j : ι
hij : i ≠ j
L₁ : StrongDual ℝ (E i)
L₂ : StrongDual ℝ (E j)
⊢ cov[(⇑L₁ : (a : E i) → ℝ) ∘ X i, (⇑L₂ : (a : E j) → ℝ) ∘ X j; P] = 0

Tactic:
simpa using h i j hij ((toDual ℝ (E i)).symm L₁) ((toDual ℝ (E j)).symm L₂)

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.symm, DFunLike.coe
-- 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
⊢ 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 ι
κ : ι → 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
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
⊢ 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:
ext
-- 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 : IsProbabilityMeasure P
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:
simp
-- 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 : 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 ω)

Tactic:
have : (fun i ω j ↦ X i j ω) = fun i ↦ (ofLp ∘ (toLp 2 ∘ fun ω j ↦ X i j ω)) := by ext; simp
-- 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 :
  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 ω)
rw :
  iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ)
    (fun (i : ι) ↦ Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω)) P
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ) (fun (i : ι) (ω : Ω) (j : κ i) ↦ X i j ω) P

Tactic:
rw [this]
-- 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 : ι), Measurable.{u_4, u_4} (α := WithLp 2 ((j : κ i) → ℝ)) ofLp

Tactic:
fun_prop
-- 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 ι
refine_1 :
  HasGaussianLaw (E := (i : ι) → WithLp 2 ((j : κ i) → ℝ))
    (fun (ω : Ω) (i : ι) ↦ (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω) P
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
⊢ iIndepFun (β := fun (i : ι) ↦ (j : κ i) → ℝ)
    (fun (i : ι) ↦ Function.comp (β := WithLp 2 ((j : κ i) → ℝ)) ofLp (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)

Premises used: ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_inner, ProbabilityTheory.iIndepFun.comp
-- 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 ι
⊢ HasGaussianLaw (E := (i : ι) → WithLp 2 ((j : κ i) → ℝ))
    (fun (ω : Ω) (i : ι) ↦ (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω) P

Tactic:
hX.map_equiv (.piCongrRight (fun _ ↦ (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm))

Premises used: ContinuousLinearEquiv.symm, Real, ProbabilityTheory.HasGaussianLaw.map_equiv, OfNat.ofNat, ContinuousLinearEquiv.piCongrRight, PiLp.continuousLinearEquiv
-- 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 ι
⊢ HasGaussianLaw (E := (i : ι) → WithLp 2 ((j : κ i) → ℝ))
    (fun (ω : Ω) (i : ι) ↦ (toLp 2 ∘ fun (ω : Ω) (j : κ i) ↦ X i j ω) ω) P

Tactic:
exact hX.map_equiv (.piCongrRight (fun _ ↦ (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm))

Premises used: ContinuousLinearEquiv.symm, Real, ProbabilityTheory.HasGaussianLaw.map_equiv, OfNat.ofNat, ContinuousLinearEquiv.piCongrRight, PiLp.continuousLinearEquiv
-- 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) → ℝ)
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
⊢ 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:
rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]

Premises used: EuclideanSpace.basisFun, OrthonormalBasis.sum_repr
-- 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) → ℝ)
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
⊢ 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

Tactic:
simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]

Premises used: conj_trivial, EuclideanSpace.basisFun_repr, EuclideanSpace.basisFun_inner, Function.comp_apply
-- 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) → ℝ)
⊢ 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:
sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- 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) → ℝ)
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
⊢ 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:
refine sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- 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) → ℝ)
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
refine_2₄ refine_2₅ : Eq (α := ℝ) 0 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * 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]

Premises used: ProbabilityTheory.covariance_const_mul_right, MulZeroClass.mul_zero, ProbabilityTheory.covariance_const_mul_left