English
If s1 ⊆ s2, μ s2 ≤ μ s1, t1 ⊆ t2, μ t2 ≤ μ t1, then μ(s1 ∪ t1) = μ(s2 ∪ t2).
Русский
Если s1 ⊆ s2, μ(s2) ≤ μ(s1), t1 ⊆ t2, μ(t2) ≤ μ(t1), то μ( s1 ∪ t1 ) = μ( s2 ∪ t2 ).
LaTeX
$$$ (s1 \subseteq s2) \rightarrow (μ s2 ≤ μ s1) \rightarrow (t1 \subseteq t2) \rightarrow (μ t2 ≤ μ t1) \rightarrow μ(s1 \cup t1) = μ(s2 \cup t2) $$$
Lean4
theorem measure_iUnion_congr_of_subset {ι : Sort*} [Countable ι] {s : ι → Set α} {t : ι → Set α} (hsub : ∀ i, s i ⊆ t i)
(h_le : ∀ i, μ (t i) ≤ μ (s i)) : μ (⋃ i, s i) = μ (⋃ i, t i) :=
by
refine le_antisymm (by gcongr; apply hsub) ?_
rcases Classical.em (∃ i, μ (t i) = ∞) with (⟨i, hi⟩ | htop)
·
calc
μ (⋃ i, t i) ≤ ∞ := le_top
_ ≤ μ (s i) := (hi ▸ h_le i)
_ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _
push_neg at htop
set M := toMeasurable μ
have H : ∀ b, (M (t b) ∩ M (⋃ b, s b) : Set α) =ᵐ[μ] M (t b) :=
by
refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
·
calc
μ (M (t b)) = μ (t b) := measure_toMeasurable _
_ ≤ μ (s b) := (h_le b)
_ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
measure_mono <|
subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
((subset_iUnion _ _).trans <| subset_toMeasurable _ _)
· measurability
· rw [measure_toMeasurable]
exact htop b
calc
μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
_ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) := (measure_congr (EventuallyEq.countable_iUnion H).symm)
_ ≤ μ (M (⋃ b, s b)) := (measure_mono (iUnion_subset fun b => inter_subset_right))
_ = μ (⋃ b, s b) := measure_toMeasurable _
