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 Ω
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)
rw :
  cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))
have hX : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P
Tactic: rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
    sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
    variance_add, h, mul_zero, add_zero]
-- 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
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)
rw :
  cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)
hX : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))
have hY : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P
Tactic: rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
    sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
    variance_add, h, mul_zero, add_zero]
-- 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
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)
rw :
  cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)
hX : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P
hY : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))
have hf : Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) P
Tactic: rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
    sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
    variance_add, h, mul_zero, add_zero]
-- 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
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)
rw :
  cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)
hX : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P
hY : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P
hf : Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) P
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))
have hg : Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) P
Tactic: rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
    sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
    variance_add, h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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
⊢ (fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : κ) ↦ Y j ω
have this : IsProbabilityMeasure P
Tactic: have := hXY.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 ω))
have h₁ : ∀ (x : Ω) (x_1 : ι),
  X x_1 x = Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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
⊢ (fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : κ) ↦ Y j ω
have hX : 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 ω))
have h₁ : ∀ (x : Ω) (x_1 : κ),
  Y x_1 x = Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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 ω))
⊢ (fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : κ) ↦ Y j ω
have hY : 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 ω))
⊢ (fun (ω : Ω) (i : ι) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : κ) ↦ Y j ω
have 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 ω)
Tactic: rw [hX, hY]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 κ
⊢ 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 ω)
have 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
Tactic: refine IndepFun.comp (HasGaussianLaw.indepFun_of_covariance_inner ?_ fun x y ↦ ?_)
    (by fun_prop) (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_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
⊢ 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 ω)
have 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
Tactic: refine IndepFun.comp (HasGaussianLaw.indepFun_of_covariance_inner ?_ fun x y ↦ ?_)
    (by fun_prop) (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_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 : κ) → ℝ)
⊢ cov[fun (ω : Ω) ↦ ⟪x, (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω⟫, fun (ω : Ω) ↦
      ⟪y, (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω⟫; P] =
    0
have 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
Tactic: rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 : κ) → ℝ)
⊢ 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
have refine_2 : cov[fun (ω : Ω) ↦
    ∑ x_1 : ι,
      HMul.hMul (α := ℝ)
        ((starRingEnd ℝ : (a : ℝ) → ℝ)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι) x)
              x_1) :
          ℝ)
        (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
          ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) x_1 : EuclideanSpace ℝ ι)
          ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))),
    fun (ω : Ω) ↦
    ∑ x : κ,
      HMul.hMul (α := ℝ)
        ((starRingEnd ℝ : (a : ℝ) → ℝ)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ) y)
              x) :
          ℝ)
        (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
          ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) x : EuclideanSpace ℝ κ)
          ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ)));
    P] =
  0
Tactic: simp_rw [sum_inner, inner_smul_left]