English
If f: β→α is used, the comap ofFunction equals the outer measure built from m∘f with image/pullback relation, provided a monotone or surjective condition holds.
Русский
Если есть отображение f: β→α, то comap ofFunction совпадает с внешней мерой, построенной из m∘f, при условии монотонности или сюръекции.
LaTeX
$$$\\mathrm{comap}_f (\\text{OuterMeasure.ofFunction } m m\\_empty) = \\text{OuterMeasure.ofFunction } (\\lambda s. m (f '' s)) (by simp; simp [m\\_empty]).$$$
Lean4
/-- If `m u = ∞` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = MeasureTheory.OuterMeasure.ofFunction m m_empty`.
E.g., if `α` is an (e)metric space and `m u = ∞` on any set of diameter `≥ r`, then this lemma
implies that `μ (s ∪ t) = μ s + μ t` on any two sets such that `r ≤ edist x y` for all `x ∈ s`
and `y ∈ t`. -/
theorem ofFunction_union_of_top_of_nonempty_inter {s t : Set α}
(h : ∀ u, (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞) :
OuterMeasure.ofFunction m m_empty (s ∪ t) =
OuterMeasure.ofFunction m m_empty s + OuterMeasure.ofFunction m m_empty t :=
by
refine le_antisymm (measure_union_le _ _) (le_iInf₂ fun f hf ↦ ?_)
set μ := OuterMeasure.ofFunction m m_empty
rcases Classical.em (∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty) with (⟨i, hs, ht⟩ | he)
·
calc
μ s + μ t ≤ ∞ := le_top
_ = m (f i) := (h (f i) hs ht).symm
_ ≤ ∑' i, m (f i) := ENNReal.le_tsum i
set I := fun s => {i : ℕ | (s ∩ f i).Nonempty}
have hd : Disjoint (I s) (I t) := disjoint_iff_inf_le.mpr fun i hi => he ⟨i, hi⟩
have hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' i : I u, μ (f i) := fun u hu =>
calc
μ u ≤ μ (⋃ i : I u, f i) :=
μ.mono fun x hx =>
let ⟨i, hi⟩ := mem_iUnion.1 (hf (hu hx))
mem_iUnion.2 ⟨⟨i, ⟨x, hx, hi⟩⟩, hi⟩
_ ≤ ∑' i : I u, μ (f i) := measure_iUnion_le _
calc
μ s + μ t ≤ (∑' i : I s, μ (f i)) + ∑' i : I t, μ (f i) :=
add_le_add (hI _ subset_union_left) (hI _ subset_union_right)
_ = ∑' i : ↑(I s ∪ I t), μ (f i) :=
(ENNReal.summable.tsum_union_disjoint (f := fun i => μ (f i)) hd ENNReal.summable).symm
_ ≤ ∑' i, μ (f i) :=
(ENNReal.summable.tsum_le_tsum_of_inj (↑) Subtype.coe_injective (fun _ _ => zero_le _) (fun _ => le_rfl)
ENNReal.summable)
_ ≤ ∑' i, m (f i) := ENNReal.tsum_le_tsum fun i => ofFunction_le _
