English
If μ and ν are finite measures on a space Ω, and for every nonnegative bounded Borel function f the integrals ∫ f dμ and ∫ f dν agree, then μ and ν are equal on all closed sets.
Русский
Если μ и ν — конечные меры на пространстве Ω, и для каждой неотрицательной ограниченной борелевской функции f интегралы совпадают: ∫ f dμ = ∫ f dν, то μ = ν на всех замкнутых множествах.
LaTeX
$$$\\mu F = ν F$ для всех замкнутых F, если для всех функций χ -- нетривиальных интегралов согласованы.$$
Lean4
/-- Two finite measures give equal values to all closed sets if the integrals of all bounded
continuous functions with respect to the two measures agree. -/
theorem measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure {Ω : Type*} [MeasurableSpace Ω]
[TopologicalSpace Ω] [HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ ν : Measure Ω} [IsFiniteMeasure μ]
(h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ x, f x ∂μ = ∫⁻ x, f x ∂ν) {F : Set Ω} (F_closed : IsClosed F) : μ F = ν F :=
by
have ν_finite : IsFiniteMeasure ν := by
constructor
have whole := h 1
simp only [BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_const, one_mul] at whole
simp [← whole]
have obs_μ := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed μ
have obs_ν := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed ν
simp_rw [h] at obs_μ
exact tendsto_nhds_unique obs_μ obs_ν
