-- 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
refine :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      cexp
        ((↑((L : (a : E × F) → ℝ)
                  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                    @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
              ℂ) *
            I -
          (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                            (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                          (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E × F)) → ℝ)
                  L) :
              ℂ) /
            2)
refine₁ :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
        charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
      cexp
        ((↑((L : (a : E × F) → ℝ)
                  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                    @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
              ℂ) *
            I -
          (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                            (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                          (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E × F)) → ℝ)
                  L) :
              ℂ) /
            2)
refine₂ :
  ∀ (L : StrongDual ℝ (E × F))
    (this :
      (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
          @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
        HAdd.hAdd (α := E × F) (β := E × F)
          ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
          ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)),
    charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
        charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
      cexp
        ((↑((L : (a : E × F) → ℝ)
                  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
                    @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y)) :
              ℂ) *
            I -
          (↑((((diagonalStrongDualProd (covarianceBilinDual (mE := inst_1) (Measure.map X P))
                            (covarianceBilinDual (mE := inst_6) (Measure.map Y P)) :
                          (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E × F)) → ℝ)
                  L) :
              ℂ) /
            2)
refine₃ :
  ∀ (L : StrongDual ℝ (E × F))
    (this :
      (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
          @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
        HAdd.hAdd (α := E × F) (β := E × F)
          ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
          ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)),
    charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
        charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
      cexp
          ((↑((L : (a : E × F) → ℝ)
                    ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) :
                      E × F)) :
                ℂ) *
              I -
            (↑((((covarianceBilinDual (mE := inst_1) (Measure.map X P) : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
                          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) :
                        StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F))) :
                ℂ) /
              2) *
        cexp
          ((↑((L : (a : E × F) → ℝ)
                    ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) :
                      E × F)) :
                ℂ) *
              I -
            (↑((((covarianceBilinDual (mE := inst_6) (Measure.map Y P) : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ)
                          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) :
                        StrongDual ℝ F →L[ℝ] ℝ) :
                      (a : StrongDual ℝ F) → ℝ)
                    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))) :
                ℂ) /
              2)
e_a :
  ∀ (L : StrongDual ℝ (E × F))
    (this :
      (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
          @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
        HAdd.hAdd (α := E × F) (β := E × F)
          ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
          ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)),
    charFunDual (mE := inst_1) (Measure.map X P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) =
      cexp
        ((↑((L : (a : E × F) → ℝ)
                  ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) :
                    E × F)) :
              ℂ) *
            I -
          (↑((((covarianceBilinDual (mE := inst_1) (Measure.map X P) : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
                        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) :
                      StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F))) :
              ℂ) /
            2)
⊢ ∃ (m : E × F) (f : StrongDual ℝ (E × F) →L[ℝ] StrongDual ℝ (E × F) →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
          cexp
            ((↑((L : (a : E × F) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →L[ℝ] ℝ) L : StrongDual ℝ (E × F) →L[ℝ] ℝ) :
                        (a : StrongDual ℝ (E × F)) → ℝ)
                      L) :
                  ℂ) /
                2)
have e_a₁ : ∀ (L : StrongDual ℝ (E × F))
  (this :
    (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
        @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
      HAdd.hAdd (α := E × F) (β := E × F)
        ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
        ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)),
  charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)) :
            ℂ) *
          I -
        (↑((((covarianceBilinDual (mE := inst_6) (Measure.map Y P) : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ)
                      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) :
                    StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))) :
            ℂ) /
          2)
Tactic: classical
    refine ⟨(∫ x, x ∂P.map X, ∫ y, y ∂P.map Y),
      .diagonalStrongDualProd (covarianceBilinDual (P.map X)) (covarianceBilinDual (P.map Y)),
      isPosSemidef_diagonalStrongDualProd isPosSemidef_covarianceBilinDual
        isPosSemidef_covarianceBilinDual, fun L ↦ ?_⟩
    rw [(indepFun_iff_charFunDual_prod (by fun_prop) (by fun_prop)).1 hXY]
    have : (∫ x, x ∂Measure.map X P, ∫ y, y ∂Measure.map Y P) =
        ContinuousLinearMap.inl ℝ E F (∫ x, x ∂Measure.map X P) +
        ContinuousLinearMap.inr ℝ E F (∫ y, y ∂Measure.map Y P) := by simp
    simp only [this, map_add, ofReal_add, add_mul, diagonalStrongDualProd_apply, add_div,
      add_sub_add_comm, exp_add]
    congr
    · rw [hX.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]
      · simp
      · exact hX.isGaussian_map.memLp_two_id
      · exact hX.isGaussian_map.integrable_id
    · rw [hY.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]
      · simp
      · exact hY.isGaussian_map.memLp_two_id
      · exact hY.isGaussian_map.integrable_id