awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, r • t⟫ : ℂ) * I) ∂μ)
have simp_rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑(r * ⟪x, t⟫) : ℂ) * I) ∂μ)
Tactic: simp_rw [inner_smul_right, ← real_inner_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst_2 : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ charFun (mE := mE) (Measure.map (fun (x : X) ↦ r • f x) μ) t = charFun (mE := mE) (Measure.map f μ) (r • t)
have hg : AEMeasurable (β := E) (_m := mE) (fun (x : E) ↦ r • x) (Measure.map f μ)
Tactic: rw [show (fun x ↦ r • (f x)) = (r • ·) ∘ f from rfl, ← AEMeasurable.map_map_of_aemeasurable,
    charFun_map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : OpensMeasurableSpace E
x t : E
⊢ charFun (mE := inst) (Measure.dirac x) t = cexp ((↑⟪x, t⟫ : ℂ) * I)
have rw : (@integral _ _ _ _ inst (Measure.dirac x) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) = cexp ((↑⟪x, t⟫ : ℂ) * I)
Tactic: rw [charFun_apply, integral_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : OpensMeasurableSpace E
x t : E
rw : (@integral _ _ _ _ inst (Measure.dirac x) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) = cexp ((↑⟪x, t⟫ : ℂ) * I)
⊢ charFun (mE := inst) (Measure.dirac x) t = cexp ((↑⟪x, t⟫ : ℂ) * I)
have rw₁ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp ((↑⟪x, t⟫ : ℂ) * I)
Tactic: rw [charFun_apply, integral_dirac]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)
have rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x + r, t⟫ : ℂ) * I) ∂μ)
  (∫ (a : E), cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I) ∂μ)
Tactic: rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop),
    ← integral_mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x + r, t⟫ : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I) ∂μ)
have e_f : ∀ (a : E), cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
⊢ cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I)
have e_f : cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I)
Tactic: rw [← Complex.exp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
⊢ cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I)
have e_f : (↑⟪a + r, t⟫ : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
⊢ (↑⟪a + r, t⟫ : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
have e_f : (↑(⟪a, t⟫ + ⟪r, t⟫) : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
Tactic: rw [inner_add_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
⊢ (↑(⟪a, t⟫ + ⟪r, t⟫) : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
have e_f : ((↑⟪a, t⟫ : ℂ) + (↑⟪r, t⟫ : ℂ)) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
Tactic: simp only [ofReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ r + x) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)
have simp_rw : charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)
Tactic: simp_rw [add_comm r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (hypothesis)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h : charFun μ = charFun ν
⊢ μ = ν
have h₁ : ∀ (x : E),
  Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
Tactic: simp_rw [funext_iff, charFun_eq_integral_innerProbChar] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ μ = ν
have refine_1 : ∀ (v : E),
  v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)
Tactic: refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
    ?_ ?_ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
refine_1 :
  ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)
⊢ μ = ν
have refine_2 : Continuous (Y := ℝ) fun (p : E × E) ↦
  ((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) p.1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) p.2
Tactic: refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
    ?_ ?_ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
⊢ ∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)
have rw : ∫ (x : E), ∫ (y : E), cexp ((↑⟪x + y, t⟫ : ℂ) * I) ∂ν ∂μ =
  HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)
Tactic: rw [integral_conv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
rw :
  ∫ (x : E), ∫ (y : E), cexp ((↑⟪x + y, t⟫ : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)
⊢ ∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)
have rw₁ : Integrable (ε := ℂ) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) (μ ∗ ν)
Tactic: rw [integral_conv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : SFinite μ
inst_5 : SFinite ν
t : WithLp 2 (E × F)
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
    charFun μ t.ofLp.1 * charFun ν t.ofLp.2
have simp_rw : Eq (α := ℂ)
  (∫ (x : E × F),
    cexp
      ((↑(⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).1, t.ofLp.1⟫ +
              ⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).2, t.ofLp.2⟫) :
          ℂ) *
        I) ∂μ.prod ν)
  (∫ (z : E × F), cexp ((↑⟪z.1, t.ofLp.1⟫ : ℂ) * I) * cexp ((↑⟪z.2, t.ofLp.2⟫ : ℂ) * I) ∂μ.prod ν)
Tactic: simp_rw [charFun, prod_inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_prod_mul,
    integral_map_equiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
⊢ ξ = μ.prod ν
have refine : ∀ (t : WithLp 2 (E × F)),
  charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t
Tactic: refine (MeasurableEquiv.toLp 2 (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t
have rw : charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
rw :
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t
have rw₁ : charFun μ t.ofLp.1 * charFun ν t.ofLp.2 =
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
rw :
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
rw₁ :
  charFun μ t.ofLp.1 * charFun ν t.ofLp.2 =
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t
have rw₂ : charFun μ t.ofLp.1 * charFun ν t.ofLp.2 = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
have rw : ∀ (t : WithLp 2 (E × F)),
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
    charFun μ t.ofLp.1 * charFun ν t.ofLp.2
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
    ∏ i : ι, charFun (μ i) (t.ofLp i)
have simp_rw : Eq (α := ℂ)
  (∫ (x : (i : ι) → E i),
    cexp
      ((↑(∑ i : ι,
              ⟪ofLp (p := 2)
                  ((MeasurableEquiv.toLp 2 ((i : ι) → E i) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) x) i,
                t.ofLp i⟫) :
          ℂ) *
        I) ∂Measure.pi (α := E) μ)
  (∫ (x : (i : ι) → E i), ∏ i : ι, cexp ((↑⟪x i, t.ofLp i⟫ : ℂ) * I) ∂Measure.pi (α := E) μ)
Tactic: simp_rw [charFun, PiLp.inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_fintype_prod_eq_prod,
    integral_map_equiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
⊢ ν = Measure.pi (α := E) μ
have refine : ∀ (t : WithLp 2 ((i : ι) → E i)),
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      t
Tactic: refine (MeasurableEquiv.toLp 2 (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      t
have rw : charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
rw :
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      t
have rw₁ : ∏ i : ι, charFun (μ i) (t.ofLp i) =
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
rw :
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
rw₁ :
  ∏ i : ι, charFun (μ i) (t.ofLp i) =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      t
have rw₂ : Eq (α := ℂ) (∏ i : ι, charFun (μ i) (t.ofLp i)) (∏ i : ι, charFun (μ i) (t.ofLp i))
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFun_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
have rw : ∀ (t : WithLp 2 ((i : ι) → E i)),
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
    ∏ i : ι, charFun (μ i) (t.ofLp i)
Tactic: rw [h]