English
For IsFiniteMeasure ν, h₁ measurable s, h₂ ν ≤ μ, we have (μ − ν)(s) = μ(s) − ν(s).
Русский
Для IsFiniteMeasure ν, измеримый_s s, ν ≤ μ: (μ − ν)(s) = μ(s) − ν(s).
LaTeX
$$$[IsFiniteMeasure \\\\nu] \\\\Rightarrow \\\\text{MeasurableSet } s \\\\Rightarrow \\\\nu \\\\le \\\\mu \\\\Rightarrow (\\\\mu - \\\\nu)(s) = \\\\mu(s) - \\\\nu(s)$$$
Lean4
/-- This application lemma only works in special circumstances. Given knowledge of
when `μ ≤ ν` and `ν ≤ μ`, a more general application lemma can be written. -/
theorem sub_apply [IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ μ) : (μ - ν) s = μ s - ν s := by
-- We begin by defining `measure_sub`, which will be equal to `(μ - ν)`.
let measure_sub : Measure α :=
MeasureTheory.Measure.ofMeasurable (fun (t : Set α) (_ : MeasurableSet t) => μ t - ν t) (by simp)
(fun g h_meas h_disj ↦ by
simp only [measure_iUnion h_disj h_meas]
rw [ENNReal.tsum_sub _ (h₂ <| g ·)]
rw [← measure_iUnion h_disj h_meas]
apply measure_ne_top)
-- Now, we demonstrate `μ - ν = measure_sub`, and apply it.
have h_measure_sub_add : ν + measure_sub = μ :=
by
ext1 t h_t_measurable_set
simp only [Pi.add_apply, coe_add]
rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm, tsub_add_cancel_of_le (h₂ t)]
have h_measure_sub_eq : μ - ν = measure_sub :=
by
rw [MeasureTheory.Measure.sub_def]
apply le_antisymm
· apply sInf_le
simp [le_refl, add_comm, h_measure_sub_add]
apply le_sInf
intro d h_d
rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d
apply Measure.le_of_add_le_add_left h_d
rw [h_measure_sub_eq]
apply Measure.ofMeasurable_apply _ h₁
