-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_2
inst_1 : Fintype ι
inst_2 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_7 : (i : ι) → NormedSpace ℝ (E i)
inst_8 : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
rw :
  Eq (α := Measure ((i : ι) → E i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
      (Measure.pi (α := E) fun (i : ι) ↦ Measure.map (X i) P) ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
rw₁ :
  (∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
      charFunDual (mE := measurableSpace p ((i : ι) → E i))
          (Measure.map (toLp p) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))) ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
rw₂ :
  (∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
      charFunDual (mE := measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))) ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
rw₃ rw₄ :
  (∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
      charFunDual (mE := measurableSpace p ((i : ι) → E i)) (Measure.map (fun (x : Ω) ↦ toLp p fun (i : ι) ↦ X i x) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))) ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
⊢ iIndepFun (β := E) X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

Premises used: Function.comp_def, MeasureTheory.charFunDual_eq_pi_iff', AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map