-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
inst_1 : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
mF : MeasurableSpace F
inst_5 : NormedAddCommGroup F
inst_6 : CompleteSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_9 : NormedSpace ℝ E
inst_10 : NormedSpace ℝ F
inst_11 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
rw :
  Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
      (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)
rw₁ :
  (∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (toLp p) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P))
          L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)) ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)
rw₂ :
  (∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (toLp p ∘ fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)) ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)
rw₃ rw₄ :
  (∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (x : Ω) ↦ toLp p (X x, Y x)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)) ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (mE := measurableSpace p (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inl ℝ E F) *
          charFunDual (mE := mF) (Measure.map Y P)
            (L ∘SL
              (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
                ContinuousLinearMap.inr ℝ E F)

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

Premises used: Function.comp_def, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, MeasureTheory.charFunDual_eq_prod_iff'