awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ X i ⟂ᵢ[P] ∑ x ∈ s, X x
have insert : (∑ x ∈ s, X x) ⟂ᵢ[P] X i
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ (∑ x ∈ s, X x) ⟂ᵢ[P] X i
have h : Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
Tactic: 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)
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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)
⊢ Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
have h : Set.InjOn (Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)) (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))
Tactic: convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
⊢ Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
have h₁ : Set.MapsTo (Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)) (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s))
  (↑s : Set ι)
Tactic: convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 ι)
⊢ Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
have 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
Tactic: convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
have 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 : ι)
Tactic: convert! (Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 ∉ Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s) '' (↑{x : ↥(insert i s) | (↑x : ι) ∈ s} : Set ↥(insert i s)) →
      X i_1 = 0
have h : ∀ i_1 ∈ s, (i_1 = i ∨ i_1 ∈ s → i_1 ∈ s → ¬i_1 = i ∧ i_1 ∉ s) → X i_1 = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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))
have 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))
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
Cleared hypotheses: mX, hX
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
⊢ 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))
have 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 i s, AEMeasurable (X i_1) P)
  (hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P),
  Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ insert i s, X i) P))
    (∏ i ∈ insert 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
Cleared hypotheses: mX, hX
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
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))
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
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) P))
    (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
have h : ∀ (x : Ω), Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! hX.charFunDual_map_finsetSum_eq_prod mX
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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) → ℂ)
    (charFunDual (mE := inst)
      (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFunDual (μ i))
have 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))
Tactic: rw [iIndepFun.charFunDual_map_fun_sum_eq_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
⊢ 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))
have mX : ∀ (i : ι), AEMeasurable (β := E) (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)
Tactic: rw [iIndepFun.charFunDual_map_fun_sum_eq_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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) μ)
⊢ 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))
have hX : iIndepFun (β := fun (x : ι) ↦ E) (fun (i : ι) (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)
Tactic: rw [iIndepFun.charFunDual_map_fun_sum_eq_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
have 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))
Tactic: refine Finset.prod_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ)
    (charFunDual (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (charFunDual (μ i))
have rw : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (μ i)) (charFunDual (μ i))
Tactic: rw [(measurePreserving_eval μ i).map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) P))
    (∏ i ∈ s, charFun (mE := inst) (Measure.map (X i) P))
have h : ∀ (x : Ω), Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! hX.charFun_map_finsetSum_eq_prod mX
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 : InnerProductSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ Eq.{u_3 + 1} (α := (t : E) → ℂ)
    (charFun (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFun (μ i))
have h : ∀ (x : E),
  charFun (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)) x =
    (∏ i : ι, charFun (μ i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_6 : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun (β := E) X P ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
have rw : Eq (α := Measure ((i : ι) → E i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (Measure.pi (α := E) fun (i : ι) ↦ Measure.map (X i) P) ↔
  ∀ (t : WithLp 2 ((x : ι) → E x)),
    charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
      ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFun_eq_pi_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]