English
Restricting the subtraction to a measurable set s commutes with subtraction: (μ − ν).restrict s = μ.restrict s − ν.restrict s for MeasurableSet s.
Русский
Ограничение вычитания к измеримому множеству s коммутирует: (μ − ν).restrict s = μ.restrict s − ν.restrict s для MeasurableSet s.
LaTeX
$$$\\\\forall s \\\\text{ MeasurableSet}, \\\\ (\\\\mu - \\\\nu)\\\\restriction s = \\\\mu\\\\restriction s - \\\\nu\\\\restriction s$$$
Lean4
theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) :
(μ - ν).restrict s = μ.restrict s - ν.restrict s :=
by
repeat rw [sub_def]
have h_nonempty : {d | μ ≤ d + ν}.Nonempty := ⟨μ, Measure.le_add_right le_rfl⟩
rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]
apply le_antisymm
· refine sInf_le_sInf_of_isCoinitialFor ?_
intro ν' h_ν'_in
rw [mem_setOf_eq] at h_ν'_in
refine ⟨ν'.restrict s, ?_, restrict_le_self⟩
refine ⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩
· rw [mem_setOf_eq, add_right_comm, Measure.le_iff]
intro t h_meas_t
repeat rw [← measure_inter_add_diff t h_meas_s]
refine add_le_add ?_ ?_
· rw [add_apply, add_apply]
apply le_add_right _
rw [← restrict_eq_self μ inter_subset_right, ← restrict_eq_self ν inter_subset_right]
apply h_ν'_in
· rw [add_apply, restrict_apply (h_meas_t.diff h_meas_s), diff_eq, inter_assoc, inter_self, ← add_apply]
have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top]
exact Measure.le_iff'.1 h_mu_le_add_top _
· ext1 t h_meas_t
simp [restrict_apply h_meas_t, restrict_apply (h_meas_t.inter h_meas_s), inter_assoc]
· refine sInf_le_sInf_of_isCoinitialFor ?_
refine forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩
rw [Set.mem_setOf_eq, ← restrict_add]
exact restrict_mono Subset.rfl h_t_in
