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 Ω
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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))
have 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
Tactic: ext L
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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
have 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
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFunDual_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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
have 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
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFunDual_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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
have 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
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFunDual_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ charFunDual (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
have mX : AEMeasurable Prod.fst (μ.prod ν)
Tactic: rw [IndepFun.charFunDual_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
⊢ charFunDual (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
have mY : AEMeasurable Prod.snd (μ.prod ν)
Tactic: rw [IndepFun.charFunDual_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
mY : AEMeasurable Prod.snd (μ.prod ν)
⊢ charFunDual (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
have hXY : Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Tactic: rw [IndepFun.charFunDual_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 : NormedSpace ℝ E
inst_9 : NormedSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
have rw : Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
    (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      charFunDual (mE := mE) (Measure.map X P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual (mE := mF) (Measure.map Y P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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 : NormedSpace ℝ E
inst_9 : NormedSpace ℝ 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)) ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
have rw₁ : (∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      charFunDual (mE := mE) (Measure.map X P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual (mE := mF) (Measure.map Y P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))) ↔
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      charFunDual (mE := mE) (Measure.map X P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual (mE := mF) (Measure.map Y P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (hypothesis)
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 this : IsProbabilityMeasure P
Tactic: have := hX.isProbabilityMeasure
-- 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
this : IsProbabilityMeasure P
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))
have empty : ∀ (x : StrongDual ℝ E),
  charFunDual (mE := inst) (Measure.map (∑ i ∈ ∅, X i) P) x =
    (∏ i ∈ ∅, charFunDual (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_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
⊢ 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))
have insert : ∀ i ∈ s, AEMeasurable (X i) P
Tactic: rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
-- 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.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
insert : ∀ i ∈ s, AEMeasurable (X i) 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))
have insert₁ : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
Tactic: rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
-- 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.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
insert : ∀ i ∈ s, AEMeasurable (X i) P
insert₁ : 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 ∈ Insert.insert i s, X i) P))
    (∏ i ∈ Insert.insert i s, charFunDual (mE := inst) (Measure.map (X i) P))
have insert₂ : AEMeasurable (X i) P
Tactic: rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
-- 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.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
insert : ∀ i ∈ s, AEMeasurable (X i) P
insert₁ : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
insert₂ : AEMeasurable (X i) 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))
have insert₃ : AEMeasurable.{u_1, u_3} (β := E) (∑ x ∈ s, X x) P
Tactic: rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]
-- 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.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
insert : ∀ i ∈ s, AEMeasurable (X i) P
insert₁ : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
insert₂ : AEMeasurable (X i) P
insert₃ : AEMeasurable.{u_1, u_3} (β := E) (∑ x ∈ s, X 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))
have insert₄ : X i ⟂ᵢ[P] ∑ x ∈ s, X x
Tactic: rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]