awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : ((t : ↥J) → F (↑t : T)) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ)) x ∂P)
J : Finset T
⊢ AEMeasurable Z P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : ((t : ↥J) → F (↑t : T)) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ)) x ∂P)
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (β := F (↑t : T)) (Y (↑t : T)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ)
          (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S)))
          ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S))) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ)
          (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S)))
          ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S))) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
I : Finset S
⊢ AEMeasurable U P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
I : Finset S
⊢ AEMeasurable U P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (I : Finset S) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (I : Finset S) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P
I : Finset S
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
𝒜 : Set (Set Ω)
m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ A ∈ 𝒜,
    ∀ (I : Finset S) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ),
      ∫ (ω : Ω) in A, ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P =
        P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P
⊢ IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P

Tactic:
indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_process_of_prod_bcf (m𝒜 A hA) mX (h A hA))

Premises used: Iff.mpr, ProbabilityTheory.indepSets_iff_singleton_indepSets, indicator_indepFun_process_of_prod_bcf, IndepFun.singleton_indepSets_of_indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
𝒜 : Set (Set Ω)
m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ A ∈ 𝒜,
    ∀ (I : Finset S) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ),
      ∫ (ω : Ω) in A, (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P =
        P.real A * ∫ (ω : Ω), (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P
⊢ IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P

Tactic:
indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_process_of_bcf (m𝒜 A hA) mX (h A hA))

Premises used: Iff.mpr, indicator_indepFun_process_of_bcf, ProbabilityTheory.indepSets_iff_singleton_indepSets, IndepFun.singleton_indepSets_of_indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
m mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
hm : m ≤ mΩ
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (A : Set Ω),
    MeasurableSet A →
      ∀ (I : Finset S) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ),
        ∫ (ω : Ω) in A, ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P =
          P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s : (a : E (↑s : S)) → ℝ) (X (↑s : S) ω) ∂P
⊢ Indep m (MeasurableSpace.comap (β := (s : S) → E s) (fun (ω : Ω) (s : S) ↦ X s ω) (MeasurableSpace.pi (X := E))) P

Tactic:
(Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_process_of_prod_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

Premises used: Iff.mpr, MeasurableSet.nullMeasurableSet, ProbabilityTheory.Indep_iff_IndepSets, indepSets_comap_process_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
m mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
hm : m ≤ mΩ
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (A : Set Ω),
    MeasurableSet A →
      ∀ (I : Finset S) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ),
        ∫ (ω : Ω) in A, (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P =
          P.real A * ∫ (ω : Ω), (f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω ∂P
⊢ Indep m (MeasurableSpace.comap (β := (s : S) → E s) (fun (ω : Ω) (s : S) ↦ X s ω) (MeasurableSpace.pi (X := E))) P

Tactic:
(Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_process_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

Premises used: Iff.mpr, MeasurableSet.nullMeasurableSet, indepSets_comap_process_of_bcf, ProbabilityTheory.Indep_iff_IndepSets
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
h :
  ∀ (t : E),
    charFun (mE := mE) (Measure.map (X + Y) P) t =
      (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
⊢ charFun (mE := mE) (Measure.map (X + Y) P) =
    charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)

Tactic:
ext t
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
h :
  charFun (mE := mE) (Measure.map X P ∗ Measure.map Y P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
h₁ :
  charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
h₂ h₃ :
  charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t =
    charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t
⊢ charFun (mE := mE) (Measure.map (X + Y) P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t

Tactic:
rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFun_conv, Pi.mul_apply]

Premises used: Pi.mul_apply, MeasureTheory.charFun_conv, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFun (mE := mE) (Measure.map (fun (ω : Ω) ↦ X ω + Y ω) P) =
    charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)

Tactic:
hXY.charFun_map_add_eq_mul mX mY

Premises used: ProbabilityTheory.IndepFun.charFun_map_add_eq_mul
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
mY : AEMeasurable Prod.snd (μ.prod ν)
hXY : Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
⊢ charFun (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) = charFun μ * charFun ν

Tactic:
rw [IndepFun.charFun_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_snd, ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul, MeasureTheory.measurePreserving_fst
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
indepFun_prod (X := id) (Y := id) measurable_id measurable_id

Premises used: ProbabilityTheory.indepFun_prod, measurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
exact indepFun_prod (X := id) (Y := id) measurable_id measurable_id

Premises used: ProbabilityTheory.indepFun_prod, measurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (α := E × F) (β := WithLp 2 (E × F)) (_m := Prod.instMeasurableSpace) (toLp 2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (β := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : 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)) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
rw₁ :
  (∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (toLp 2) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
rw₂ :
  (∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (toLp 2 ∘ fun (ω : Ω) ↦ (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
rw₃ rw₄ :
  (∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (x : Ω) ↦ toLp 2 (X x, Y x)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2

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

Premises used: MeasureTheory.charFun_eq_prod_iff, Function.comp_def, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual (mE := mE) (Measure.map (X + Y) P) L =
      HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (β := (L : StrongDual ℝ E) → ℂ)
        (charFunDual (mE := mE) (Measure.map X P)) (charFunDual (mE := mE) (Measure.map Y P)) L
⊢ charFunDual (mE := mE) (Measure.map (X + Y) P) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := mE) (Measure.map X P))
      (charFunDual (mE := mE) (Measure.map Y P))

Tactic:
ext L
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
h :
  charFunDual (mE := mE) (Measure.map X P ∗ Measure.map Y P) L =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (β := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := mE) (Measure.map X P))
      (charFunDual (mE := mE) (Measure.map Y P)) L
h₁ :
  charFunDual (mE := mE) (Measure.map X P) L * charFunDual (mE := mE) (Measure.map Y P) L =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (β := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := mE) (Measure.map X P))
      (charFunDual (mE := mE) (Measure.map Y P)) L
h₂ h₃ :
  charFunDual (mE := mE) (Measure.map X P) L * charFunDual (mE := mE) (Measure.map Y P) L =
    charFunDual (mE := mE) (Measure.map X P) L * charFunDual (mE := mE) (Measure.map Y P) L
⊢ charFunDual (mE := mE) (Measure.map (X + Y) P) L =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (β := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := mE) (Measure.map X P))
      (charFunDual (mE := mE) (Measure.map Y P)) L

Tactic:
rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFunDual_conv, Pi.mul_apply]

Premises used: Pi.mul_apply, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀, MeasureTheory.charFunDual_conv