ext_of_complexMGF_id_eq — Mathlib

English

If the complex MGFs of the identity with respect to μ and μ' coincide, then μ = μ'.

Русский

Если MGФ для тождественного отображения по мере μ совпадает с MGФ для μ', тогда меры равны.

LaTeX

$$$\\text{complexMGF}(\\mathrm{id}, μ) = \\text{complexMGF}(\\mathrm{id}, μ') \\Rightarrow μ = μ'$$$

Lean4

theorem _root_.MeasureTheory.Measure.ext_of_complexMGF_id_eq {μ μ' : Measure ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure μ']
    (h : complexMGF id μ = complexMGF id μ') : μ = μ' := by
  simpa using Measure.ext_of_complexMGF_eq aemeasurable_id aemeasurable_id h

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