∀ {ι : Type u_6} [inst : Fintype ι] {E : ι → Type u_7} [inst_1 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_2 : (i : ι) → InnerProductSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), CompleteSpace (E i)]
  [∀ (i : ι), SecondCountableTopology (E i)] [∀ (i : ι), BorelSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)}
  {ν : MeasureTheory.Measure ((i : ι) → E i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (t : WithLp 2 ((i : ι) → E i)),
      MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) ν) t =
        ∏ i, MeasureTheory.charFun (μ i) (t.ofLp i)) ↔
    ν = MeasureTheory.Measure.pi μ