English
The negation operation preserves mutual singularity: -s ⟂ᵥ w in the signed measure context.
Русский
Операция отрицания сохраняет взаимную обособленность: -s ⟂ᵥ w.
LaTeX
$$$ (-s) \\perp_{\\mathcal{V}} w $$$
Lean4
/-- Given a signed measure `s` and a positive measurable set `i`, `toMeasureOfZeroLE`
provides the measure, mapping measurable sets `j` to `s (i ∩ j)`. -/
def toMeasureOfZeroLE (s : SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) : Measure α :=
by
refine Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ?_ ?_
· simp_rw [toMeasureOfZeroLE', s.restrict_apply hi₁ MeasurableSet.empty, Set.empty_inter i, s.empty]
rfl
· intro f hf₁ hf₂
have h₁ : ∀ n, MeasurableSet (i ∩ f n) := fun n => hi₁.inter (hf₁ n)
have h₂ : Pairwise (Disjoint on fun n : ℕ => i ∩ f n) :=
by
intro n m hnm
exact ((hf₂ hnm).inf_left' i).inf_right' i
simp only [toMeasureOfZeroLE', s.restrict_apply hi₁ (MeasurableSet.iUnion hf₁), Set.inter_comm, Set.inter_iUnion,
s.of_disjoint_iUnion h₁ h₂]
have h : ∀ n, 0 ≤ s (i ∩ f n) := fun n =>
s.nonneg_of_zero_le_restrict (s.zero_le_restrict_subset hi₁ Set.inter_subset_left hi₂)
rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]
· refine tsum_congr fun n => ?_
simp_rw [s.restrict_apply hi₁ (hf₁ n), Set.inter_comm]
· exact (NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable
