awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
h :
  Set.InjOn (Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)) (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))
h₁ :
  Set.MapsTo (Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)) (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))
    (↑s : Set ι)
h₂ :
  ∀ i_1 ∈ s,
    i_1 ∉ Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s) '' (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s)) →
      X i_1 = 0
h₃ :
  ∀ (i_1 : ↥(insert i s)),
    Membership.mem (γ := Finset ↥(insert i s)) {x : ↥(insert i s) | (↑x : ι) ∈ s} i_1 → X (↑i_1 : ι) = X (↑i_1 : ι)
⊢ Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))

Tactic:
convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm

Premises used: Finset.sum_of_injOn, Eq.symm, Subtype.val
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
⊢ Set.InjOn (Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)) (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))

Tactic:
simp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
x : ↥(insert i s)
h : x ∈ (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s)) → (↑x : ι) ∈ (↑s : Set ι)
⊢ x ∈ (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s)) → (↑x : ι) ∈ (↑s : Set ι)

Tactic:
_
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
x : ↥(insert i s)
h : x ∈ (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))
⊢ (↑x : ι) ∈ (↑s : Set ι)

Tactic:
grind
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
h : ∀ i_1 ∈ s, (i_1 = i ∨ i_1 ∈ s → i_1 ∈ s → ¬i_1 = i ∧ i_1 ∉ s) → X i_1 = 0
⊢ ∀ i_1 ∈ s,
    i_1 ∉ Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s) '' (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s)) →
      X i_1 = 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
⊢ ∀ i_1 ∈ s, (i_1 = i ∨ i_1 ∈ s → i_1 ∈ s → ¬i_1 = i ∧ i_1 ∉ s) → X i_1 = 0

Tactic:
grind
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
⊢ ∀ (i_1 : ↥(insert i s)),
    Membership.mem (γ := Finset ↥(insert i s)) {x : ↥(insert i s) | (↑x : ι) ∈ s} i_1 → X (↑i_1 : ι) = X (↑i_1 : ι)

Tactic:
grind
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
this : IsProbabilityMeasure P
empty :
  ∀ (mX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥∅) ↦ E) (Finset.restrict (π := fun (i : ι) ↦ Ω → E) ∅ X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ ∅, X i) P))
      (∏ i ∈ ∅, charFunDual (mE := inst) (Measure.map (X i) P))
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (hs :
      ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
        (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
        Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
          (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P)))
    (mX : ∀ i_1 ∈ Insert.insert i s, AEMeasurable (X i_1) P)
    (hX :
      iIndepFun (β := fun (x : ↥(Insert.insert i s)) ↦ E) ((Insert.insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X)
        P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ)
      (charFunDual (mE := inst) (Measure.map (∑ i ∈ Insert.insert i s, X i) P))
      (∏ i ∈ Insert.insert i s, charFunDual (mE := inst) (Measure.map (X i) P))
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
    (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
induction s using Finset.induction with
  | empty => ext; simp [show (0 : Ω → E) = fun _ ↦ 0 from rfl]
  | insert i s hi hs =>
    rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
    · exact fun i hi ↦ (mX i (mem_insert_of_mem hi))
    · exact hX.precomp (g := fun x : s ↦ ⟨x.1, mem_insert_of_mem x.2⟩) (fun _ ↦ by simp)
    · exact mX i (mem_insert_self i s)
    · exact Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))
    symm
    convert!
      iIndepFun.indepFun_finsetSum_of_notMem₀ (i := ⟨i, mem_insert_self i s⟩) (f :=
        fun (x : (insert i s : Finset ι)) ↦ X x.1) (s := {x | x.1 ∈ s}) hX (fun i ↦ (mX i.1 i.2))
        (by simpa)
    let e : ((insert i s) : Finset ι) → ι := Subtype.val
    convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
    · simp
    · intro _ _; grind
    · simp; grind
    · grind

Premises used: Finset.sum_of_injOn, Insert.insert, ProbabilityTheory.iIndepFun.precomp, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, Eq.symm, Subtype.val, Finset.aemeasurable_sum, rfl
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
have have₁ have₂ :
  ∀ (this : IsProbabilityMeasure P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
    (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
classical
  have := hX.isProbabilityMeasure
  induction s using Finset.induction with
  | empty => ext; simp [show (0 : Ω → E) = fun _ ↦ 0 from rfl]
  | insert i s hi hs =>
    rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
    · exact fun i hi ↦ (mX i (mem_insert_of_mem hi))
    · exact hX.precomp (g := fun x : s ↦ ⟨x.1, mem_insert_of_mem x.2⟩) (fun _ ↦ by simp)
    · exact mX i (mem_insert_self i s)
    · exact Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))
    symm
    convert!
      iIndepFun.indepFun_finsetSum_of_notMem₀ (i := ⟨i, mem_insert_self i s⟩) (f :=
        fun (x : (insert i s : Finset ι)) ↦ X x.1) (s := {x | x.1 ∈ s}) hX (fun i ↦ (mX i.1 i.2))
        (by simpa)
    let e : ((insert i s) : Finset ι) → ι := Subtype.val
    convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
    · simp
    · intro _ _; grind
    · simp; grind
    · grind

Premises used: Finset.sum_of_injOn, Insert.insert, ProbabilityTheory.iIndepFun.precomp, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, Eq.symm, Subtype.val, rfl
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
mX : ∀ (i : ι), AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ι) ↦ E) X P
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → AEMeasurable (X i) P

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
    (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
hX.charFunDual_map_finsetSum_eq_prod mX

Premises used: ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
h : ∀ (x : Ω), Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) P))
    (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
convert! hX.charFunDual_map_finsetSum_eq_prod mX

Premises used: ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
x : Ω
⊢ Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
rw :
  Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ)
    (∏ i : ι,
      charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFunDual (μ i))
mX : ∀ (i : ι), AEMeasurable (β := E) (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)
hX : iIndepFun (β := fun (x : ι) ↦ E) (fun (i : ι) (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ)
    (charFunDual (mE := inst)
      (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFunDual (μ i))

Tactic:
rw [iIndepFun.charFunDual_map_fun_sum_eq_prod]

Premises used: ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ)
    (∏ i : ι,
      charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFunDual (μ i))

Tactic:
Finset.prod_congr rfl fun i _ ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      Eq (α := (L : StrongDual ℝ E) → ℂ)
        (charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
        (charFunDual (μ i))
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ)
    (∏ i : ι,
      charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFunDual (μ i))

Tactic:
refine Finset.prod_congr rfl fun i _ ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
rw rw₁ : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (μ i)) (charFunDual (μ i))
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ)
    (charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (charFunDual (μ i))

Tactic:
rw [(measurePreserving_eval μ i).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι), AEMeasurable (β := E) (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)

Tactic:
aemeasurable_id.eval

Premises used: aemeasurable_id, AEMeasurable.eval
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι), AEMeasurable (β := E) (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)

Tactic:
exact aemeasurable_id.eval

Premises used: aemeasurable_id, AEMeasurable.eval
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ iIndepFun (β := fun (x : ι) ↦ E) (fun (i : ι) (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)

Tactic:
iIndepFun_pi (X := fun _ ↦ id) (fun _ ↦ aemeasurable_id)

Premises used: ProbabilityTheory.iIndepFun_pi, aemeasurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : NormedSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ iIndepFun (β := fun (x : ι) ↦ E) (fun (i : ι) (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)

Tactic:
exact iIndepFun_pi (X := fun _ ↦ id) (fun _ ↦ aemeasurable_id)

Premises used: ProbabilityTheory.iIndepFun_pi, aemeasurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
h :
  ∀ (x : E),
    charFun (mE := inst) (Measure.map (∑ i ∈ s, X i) P) x = (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P)) x
⊢ Eq.{u_3 + 1} (α := (t : E) → ℂ) (charFun (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
    (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P))

Tactic:
ext
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
x : E
⊢ charFun (mE := inst) (Measure.map (∑ i ∈ s, X i) P) x = (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P)) x

Tactic:
simp [charFun_eq_charFunDual_toDualMap, hX.charFunDual_map_finsetSum_eq_prod mX]

Premises used: MeasureTheory.charFun_eq_charFunDual_toDualMap, ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : Fintype ι
inst_5 : InnerProductSpace ℝ E
mX : ∀ (i : ι), AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ι) ↦ E) X P
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → AEMeasurable (X i) P

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ Eq.{u_3 + 1} (α := (t : E) → ℂ) (charFun (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
    (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P))

Tactic:
hX.charFun_map_finsetSum_eq_prod mX

Premises used: ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
h : ∀ (x : Ω), Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
⊢ Eq.{u_3 + 1} (α := (t : E) → ℂ) (charFun (mE := inst) (Measure.map (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) P))
    (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P))

Tactic:
convert! hX.charFun_map_finsetSum_eq_prod mX

Premises used: ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod