ext_of_charFun — Mathlib

English

If the characteristic functions of two finite measures μ and ν coincide, then μ = ν.

Русский

Если χ_μ = χ_ν тогда μ = ν для соответствующих условий.

LaTeX

$$$$\\chi_{\\mu} = \\chi_{\\nu} \\Rightarrow \\mu = \\nu.$$$$

Lean4

/-- If the characteristic functions `charFun` of two finite measures `μ` and `ν` on
a complete second-countable inner product space coincide, then `μ = ν`. -/
theorem ext_of_charFun [CompleteSpace E] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : charFun μ = charFun ν) : μ = ν :=
  by
  simp_rw [funext_iff, charFun_eq_integral_innerProbChar] at h
  refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := bilinFormOfRealInner) ?_ ?_ h
  · exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩
  · exact continuous_inner

Похожие утверждения