∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} [BorelSpace E] [SecondCountableTopology E] (p : ENNReal) [inst_6 : Fact (1 ≤ p)]
  [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E] [CompleteSpace F] {ξ : MeasureTheory.Measure (E × F)}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (L : StrongDual ℝ (WithLp p (E × F))),
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (WithLp.toLp p) ξ) L =
        MeasureTheory.charFunDual μ
            (ContinuousLinearMap.comp L
              ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inl ℝ E F))) *
          MeasureTheory.charFunDual ν
            (ContinuousLinearMap.comp L
              ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inr ℝ E F)))) ↔
    ξ = μ.prod ν