English
Equality of integrals across all w implies equality of the underlying probability structure P = P'.
Русский
Равенство интегралов по всем w приводит к равенству первичных структур вероятностей.
LaTeX
$$ext_of_integral_char_eq (he) (hL) (h) : P = P'$$
Lean4
/-- If the integrals of `char` with respect to two finite measures `P` and `P'` coincide, then
`P = P'`. -/
theorem ext_of_integral_char_eq (he : Continuous e) (he' : e ≠ 1) (hL' : ∀ v ≠ 0, L v ≠ 0)
(hL : Continuous fun p : V × W ↦ L p.1 p.2) {P P' : Measure V} [IsFiniteMeasure P] [IsFiniteMeasure P']
(h : ∀ w, ∫ v, char he hL w v ∂P = ∫ v, char he hL w v ∂P') : P = P' :=
by
apply
ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
(separatesPoints_charPoly he he' hL hL')
intro _ hg
simp only [mem_charPoly] at hg
obtain ⟨w, hw⟩ := hg
rw [hw]
have hsum (P : Measure V) [IsFiniteMeasure P] :
∫ v, ∑ a ∈ w.support, w a * e (L v a) ∂P = ∑ a ∈ w.support, ∫ v, w a * e (L v a) ∂P :=
integral_finset_sum w.support fun a ha => Integrable.const_mul (integrable P (char he hL a)) _
rw [hsum P, hsum P']
apply Finset.sum_congr rfl fun i _ => ?_
simp only [MeasureTheory.integral_const_mul, mul_eq_mul_left_iff]
exact Or.inl (h i)
