awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P

Tactic:
exact (hXY.fst.map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.fst, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P

Tactic:
(hXY.snd.map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P

Tactic:
exact (hXY.snd.map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) P

Tactic:
(hXY.fst.map _).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable, ProbabilityTheory.HasGaussianLaw.fst
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) P

Tactic:
exact (hXY.fst.map _).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable, ProbabilityTheory.HasGaussianLaw.fst
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) P

Tactic:
(hXY.snd.map _).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable, ProbabilityTheory.HasGaussianLaw.snd
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) P

Tactic:
exact (hXY.snd.map _).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable, ProbabilityTheory.HasGaussianLaw.snd
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : InnerProductSpace ℝ E
inst_11 : InnerProductSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (x : E) (y : F), cov[fun (ω : Ω) ↦ ⟪x, X ω⟫, fun (ω : Ω) ↦ ⟪y, Y ω⟫; P] = 0
L₁ : StrongDual ℝ E
L₂ : StrongDual ℝ F
⊢ cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0

Tactic:
simpa using h ((toDual ℝ E).symm L₁) ((toDual ℝ F).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_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
⊢ IsProbabilityMeasure P

Tactic:
have := hXY.isProbabilityMeasure
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
h₁ :
  ∀ (x : Ω) (x_1 : ι),
    X x_1 x = Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1
⊢ Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
x : Ω
x_1 : ι
⊢ X x_1 x = Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
⊢ Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))

Tactic:
have hX : (fun ω i ↦ X i ω) = (ofLp ∘ (toLp 2 ∘ fun ω i ↦ X i ω)) := by ext; simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
h₁ :
  ∀ (x : Ω) (x_1 : κ),
    Y x_1 x = Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) x x_1
⊢ Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
x : Ω
x_1 : κ
⊢ Y x_1 x = Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) x x_1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
⊢ Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))

Tactic:
have hY : (fun ω j ↦ Y j ω) = (ofLp ∘ (toLp 2 ∘ fun ω j ↦ Y j ω)) := by ext; simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
rw :
  Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P]
    Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω)
⊢ (fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : κ) ↦ Y j ω

Tactic:
rw [hX, hY]
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
⊢ Measurable.{u_4, u_4} (α := WithLp 2 ((i : ι) → ℝ)) ofLp

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
⊢ Measurable.{u_5, u_5} (α := WithLp 2 ((j : κ) → ℝ)) ofLp

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
refine_1 :
  HasGaussianLaw (E := Prod.{u_4, u_5} (WithLp 2 ((i : ι) → ℝ)) (WithLp 2 ((j : κ) → ℝ)))
    (fun (ω : Ω) ↦ ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω)) P
refine_2 :
  ∀ (x : WithLp 2 ((i : ι) → ℝ)) (y : WithLp 2 ((j : κ) → ℝ)),
    cov[fun (ω : Ω) ↦ ⟪x, (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω⟫, fun (ω : Ω) ↦
        ⟪y, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω⟫; P] =
      0
⊢ Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P]
    Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω)

Tactic:
refine IndepFun.comp (HasGaussianLaw.indepFun_of_covariance_inner ?_ fun x y ↦ ?_)
    (by fun_prop) (by fun_prop)

Premises used: ProbabilityTheory.IndepFun.comp, ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_inner
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
⊢ HasGaussianLaw (E := Prod.{u_4, u_5} (WithLp 2 ((i : ι) → ℝ)) (WithLp 2 ((j : κ) → ℝ)))
    (fun (ω : Ω) ↦ ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω)) P

Tactic:
hXY.map_equiv (.prodCongr (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm
      (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm)

Premises used: ContinuousLinearEquiv.symm, Real, setOf, Prod.map, ProbabilityTheory.HasGaussianLaw.map_equiv, OfNat.ofNat, ContinuousLinearEquiv.prodCongr, PiLp.continuousLinearEquiv
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
⊢ HasGaussianLaw (E := Prod.{u_4, u_5} (WithLp 2 ((i : ι) → ℝ)) (WithLp 2 ((j : κ) → ℝ)))
    (fun (ω : Ω) ↦ ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω)) P

Tactic:
exact hXY.map_equiv (.prodCongr (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm
      (PiLp.continuousLinearEquiv 2 ℝ (fun _ ↦ ℝ)).symm)

Premises used: ContinuousLinearEquiv.symm, Real, ProbabilityTheory.HasGaussianLaw.map_equiv, OfNat.ofNat, ContinuousLinearEquiv.prodCongr, PiLp.continuousLinearEquiv
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 :
  cov[fun (ω : Ω) ↦
      inner.{0, u_4} ℝ (E := WithLp 2 ((i : ι) → ℝ))
        (∑ i : ι,
          HSMul.hSMul (α := (fun (x : ι) ↦ ℝ) i) (β := EuclideanSpace ℝ ι)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι) x)
              i)
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω),
      fun (ω : Ω) ↦
      inner.{0, u_5} ℝ (E := WithLp 2 ((j : κ) → ℝ))
        (∑ i : κ,
          HSMul.hSMul (α := (fun (x : κ) ↦ ℝ) i) (β := EuclideanSpace ℝ κ)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ) y)
              i)
            ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) i : EuclideanSpace ℝ κ))
        ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω);
      P] =
    0
⊢ cov[fun (ω : Ω) ↦ ⟪x, (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω⟫, fun (ω : Ω) ↦
      ⟪y, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω⟫; P] =
    0

Tactic:
rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]

Premises used: EuclideanSpace.basisFun, OrthonormalBasis.sum_repr