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 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₁ :
  norm (E := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ) +
      norm (E := ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ) ≤
    sorry * ‖x‖ * ‖y‖ + sorry * ‖x‖ * ‖y‖
have h₂ : norm (E := ℝ)
    ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (y ∘SL inr ℝ E F) :
      ℝ) ≤
  sorry * ‖x‖ * ‖y‖
Tactic: gcongr
-- 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 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ norm (E := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
have h₁ : ‖L₁‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
Tactic: grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_inl_le_one]
-- 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 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖L₁‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
have h₁ : ‖L₁‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ norm (E := ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
have h₂ : ‖L₂‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
Tactic: grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_inr_le_one]
-- 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 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖L₂‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
have h₂ : ‖L₂‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x y : StrongDual ℝ (E × F)
⊢ Eq (α := ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        y :
      ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) y :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        x :
      ℝ)
have simp_rw : HAdd.hAdd (α := ℝ) (β := ℝ)
    ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (y ∘SL inl ℝ E F) :
      ℝ)
    ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (y ∘SL inr ℝ E F) :
      ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ)
    ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (y ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (x ∘SL inl ℝ E F) :
      ℝ)
    ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (y ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (x ∘SL inr ℝ E F) :
      ℝ)
Tactic: simp_rw [toBilinForm_diagonalStrongDualProd_apply, h₁.eq, h₂.eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x y : StrongDual ℝ (E × F)
simp_rw :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (y ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (x ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (y ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (x ∘SL inr ℝ E F) :
        ℝ)
⊢ Eq (α := ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        y :
      ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) y :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        x :
      ℝ)
have simp_rw₁ : HAdd.hAdd (α := ℝ) (β := ℝ)
    ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (y ∘SL inl ℝ E F) :
      ℝ)
    ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (y ∘SL inr ℝ E F) :
      ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ)
    ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (y ∘SL inl ℝ E F) :
      ℝ)
    ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (y ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (x ∘SL inr ℝ E F) :
      ℝ)
Tactic: simp_rw [toBilinForm_diagonalStrongDualProd_apply, h₁.eq, h₂.eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((L₁.diagonalStrongDualProd L₂).toBilinForm : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x :
            StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E × F)) → ℝ)
        x :
      ℝ)
have rw : 0 ≤
  HAdd.hAdd (α := ℝ) (β := ℝ)
    ((((L₁.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (x ∘SL inl ℝ E F) :
      ℝ)
    ((((L₂.toBilinForm : (a : StrongDual ℝ F) → StrongDual ℝ F →ₗ[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ F) → ℝ)
        (x ∘SL inr ℝ E F) :
      ℝ)
Tactic: rw [toBilinForm_diagonalStrongDualProd_apply]
-- 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 ι
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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
⊢ IsGaussian (E := (x : ι) → E x) (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P)
have this : IsProbabilityMeasure P
Tactic: have := hX2.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 ι
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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ IsGaussian (E := (x : ι) → E x) (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P)
have rw : ∃ (m : (x : ι) → E x) (f : StrongDual ℝ ((x : ι) → E x) →L[ℝ] StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ),
  f.toBilinForm.IsPosSemidef ∧
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
        cexp
          ((↑((L : (a : (x : ι) → E x) → ℝ) m) : ℂ) * I -
            (↑((((f : (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) L :
                        StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                      (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                    L) :
                ℂ) /
              2)
Tactic: rw [isGaussian_iff_gaussian_charFunDual]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : 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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ (m : (x : ι) → E x) (f : StrongDual ℝ ((x : ι) → E x) →L[ℝ] StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
          cexp
            ((↑((L : (a : (x : ι) → E x) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) L :
                          StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                      L) :
                  ℂ) /
                2)
have refine : ∀ (L : StrongDual ℝ ((x : ι) → E x)),
  charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)
Tactic: refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Finite ι
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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
⊢ ∀ (i : ι), AEMeasurable (X i) P
have funProp : ∀ (i : ι), AEFinStronglyMeasurable.{u_1, u_3} (β := E i) (fun (a : Ω) ↦ X i a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : 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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
⊢ charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)
have rw : ∏ i : ι,
    charFunDual (mE := inst_2 i) (Measure.map (X i) P)
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) =
  cexp
    ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
              @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
          ℂ) *
        I -
      (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                      (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                    L :
                  StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
              L) :
          ℂ) /
        2)
Tactic: rw [(iIndepFun_iff_charFunDual_pi (by fun_prop)).1 hX2]
-- 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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := E) X P
this_1 : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
⊢ ∏ i : ι,
      charFunDual (mE := inst_2 i) (Measure.map (X i) P)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) =
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ) fun (i : ι) ↦
                @integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x) :
            ℂ) *
          I -
        (↑((((diagonalStrongDualPi (E := E) fun (i : ι) ↦ covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                        (a : StrongDual ℝ ((x : ι) → E x)) → StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ)
                      L :
                    StrongDual ℝ ((x : ι) → E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ ((x : ι) → E x)) → ℝ)
                L) :
            ℂ) /
          2)
have simp : Eq (α := ℂ)
  (∏ i : ι,
    charFunDual (mE := inst_2 i) (Measure.map (X i) P)
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)))
  (∏ x : ι,
    cexp
      ((↑((L : (a : (x : ι) → E x) → ℝ)
                (Pi.single (M := E) x (@integral _ _ _ _ (inst_2 x) (Measure.map (X x) P) fun (x : E x) ↦ x))) :
            ℂ) *
          I -
        (↑((((covarianceBilinDual (mE := inst_2 x) (Measure.map (X x) P) :
                        (a : StrongDual ℝ (E x)) → StrongDual ℝ (E x) →L[ℝ] ℝ)
                      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x)) :
                    StrongDual ℝ (E x) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E x)) → ℝ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E x))) :
            ℂ) /
          2))
Tactic: simp only [← LinearMap.sum_single_apply E (fun i ↦ ∫ x, x ∂P.map (X i)), map_sum, ofReal_sum,
      sum_mul, diagonalStrongDualPi_apply, sum_div, ← sum_sub_distrib, exp_sum]