-- 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 ι
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)
refine₁ :
  ∀ (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)
refine₂ :
  ∀ (L : StrongDual ℝ ((x : ι) → E x)),
    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))
e_f :
  ∀ (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) → ℝ)
                  (Pi.single (M := E) i (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x))) :
              ℂ) *
            I -
          (↑((((covarianceBilinDual (mE := inst_2 i) (Measure.map (X i) P) :
                          (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) :
                      StrongDual ℝ (E i) →L[ℝ] ℝ) :
                    (a : StrongDual ℝ (E i)) → ℝ)
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i))) :
              ℂ) /
            2)
e_f₁ :
  ∀ (L : StrongDual ℝ ((x : ι) → E x)) (i : ι),
    cexp
        ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i) : (a : E i) → ℝ)
                  (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x)) :
              ℂ) *
            I -
          (↑(variance (mΩ := inst_2 i)
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                  (Measure.map (X i) P)) :
              ℂ) /
            2) =
      cexp
        ((↑((L : (a : (x : ι) → E x) → ℝ)
                  (Pi.single (M := E) i (@integral _ _ _ _ (inst_2 i) (Measure.map (X i) P) fun (x : E i) ↦ x))) :
              ℂ) *
            I -
          (↑(variance (mΩ := inst_2 i)
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (single ℝ E i)) : (a : E i) → ℝ)
                  (Measure.map (X i) P)) :
              ℂ) /
            2)
⊢ ∃ (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 e_f₂ : ∀ (L : StrongDual ℝ ((x : ι) → E x)) (i : ι), MemLp (m0 := inst_2 i) id 2 (Measure.map (X i) P)
Tactic: classical
    refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩
    rw [(iIndepFun_iff_charFunDual_pi (by fun_prop)).1 hX2]
    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]
    congr with i
    rw [(hX1 i).isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
      covarianceBilinDual_self_eq_variance]
    · simp
    · exact (hX1 i).isGaussian_map.memLp_two_id
    · exact (hX1 i).isGaussian_map.integrable_id