of_symmDiff_compl_positive_negative

English

The symmetric difference of two Hahn decompositions has measure zero: if i,j are measurable and (i is Hahn for s) and (j is Hahn for s), then s(i Δ j) = 0 and s(i^c Δ j^c) = 0.

Русский

Симметрическая разность двух разложений Холла имеет нулевую меру: если i,j измеримы и являются разложениями Хана для s, то s(i Δ j) = 0 и s(i^c Δ j^c) = 0.

LaTeX

$$$\forall s,i,j,\ \text{MeasurableSet}(i),\text{MeasurableSet}(j),\(0\le_i s\land s\le_{i^c}0)\land (0\le_j s\land s\le_{j^c}0)\Rightarrow s(i\triangle j)=0\land s(i^c\triangle j^c)=0.$$$

Lean4

/-- The symmetric difference of two Hahn decompositions has measure zero. -/
theorem of_symmDiff_compl_positive_negative {s : SignedMeasure α} {i j : Set α} (hi : MeasurableSet i)
    (hj : MeasurableSet j) (hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0) (hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0) :
    s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0 :=
  by
  rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
  constructor
  · rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left) (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left) (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
      zero_apply, zero_apply, zero_add]
    ·
      exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right (disjoint_comm.1 (IsCompl.disjoint isCompl_compl)))
    · exact hj.compl.inter hi
    · exact hi.compl.inter hj
  · rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, compl_compl, compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right) (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right) (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
      zero_apply, zero_apply, zero_add]
    ·
      exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right (IsCompl.disjoint isCompl_compl))
    · exact hj.inter hi.compl
    · exact hi.inter hj.compl
  all_goals measurability

Похожие утверждения