English
If two finite measures have the same dual characteristic function, they are equal.
Русский
Если две конечные меры имеют одинаковую двойственную характеристическую функцию, они равны.
LaTeX
$$$\operatorname{extOfCharFunDual}(μ, ν) \,\Rightarrow \, μ = ν$$$
Lean4
/-- If two finite measures have the same characteristic function, then they are equal. -/
theorem ext_of_charFunDual [CompleteSpace E] {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
(h : charFunDual μ = charFunDual ν) : μ = ν :=
by
refine ext_of_integral_char_eq continuous_probChar probChar_ne_one ?_ ?_ (fun L ↦ funext_iff.mp h L)
· intro v hv
rw [ne_eq, LinearMap.ext_iff]
simp only [ContinuousLinearMap.toLinearMap₁₂_apply, LinearMap.zero_apply, not_forall]
change ∃ L : StrongDual ℝ E, L v ≠ 0
by_contra! h
exact hv (NormedSpace.eq_zero_of_forall_dual_eq_zero _ h)
· exact isBoundedBilinearMap_apply.symm.continuous
