English
The infimum of μ and ν on a measurable set s equals the Inf over all decompositions μ(t∩s) + ν(t^c∩s).
Русский
На измеримом множестве s инфимум μ и ν равен Inf по всем разложениям μ(t∩s) + ν(t^c∩s).
LaTeX
$$$ (μ \\inf ν)\\,s = sInf \\{ m : ∃ t,\; m = μ(t \\cap s) + ν(t^{c} \\cap s) \\}$ for measurable s$$
Lean4
theorem inf_apply {s : Set α} (hs : MeasurableSet s) : (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} := by
-- `(μ ⊓ ν) s` is defined as `⊓ (t : ℕ → Set α) (ht : s ⊆ ⋃ n, t n), ∑' n, μ (t n) ⊓ ν (t n)`
rw [← sInf_pair, Measure.sInf_apply hs, OuterMeasure.sInf_apply (image_nonempty.2 <| insert_nonempty μ { ν })]
refine le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)
· subst ht₁
set t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅ with ht'
refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_
· by_cases hxt : x ∈ t
· refine mem_iUnion.2 ⟨0, ?_⟩
simp [hx, hxt]
· refine mem_iUnion.2 ⟨1, ?_⟩
simp [hx, hxt]
· simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero]
· exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])
· simp only [ite_eq_left_iff]
intro n hn₁ hn₀
simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, le_refl, inf_of_le_left]
· simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
-- Conversely, fixing `t' : ℕ → Set α` such that `s ⊆ ⋃ n, t' n`, we construct `t : Set α`
-- for which `μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n)`.
-- Denoting `I := {n | μ (t' n) ≤ ν (t' n)}`, we set `t = ⋃ n ∈ I, t' n`.
-- Clearly `μ (t ∩ s) ≤ ∑' n ∈ I, μ (t' n)` and `ν (tᶜ ∩ s) ≤ ∑' n ∉ I, ν (t' n)`, so
-- `μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n ∈ I, μ (t' n) + ∑' n ∉ I, ν (t' n)`
-- where the RHS equals `∑' n, μ (t' n) ⊓ ν (t' n)` by the choice of `I`.
set t := ⋃ n ∈ {k : ℕ | μ (t' k) ≤ ν (t' k)}, t' n with ht
suffices hadd : μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n) by exact le_trans (sInf_le ⟨t, rfl⟩) hadd
have hle₁ : μ (t ∩ s) ≤ ∑' (n : {k | μ (t' k) ≤ ν (t' k)}), μ (t' n) :=
(measure_mono inter_subset_left).trans <| measure_biUnion_le _ (to_countable _) _
have hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n :=
by
simp_rw [ht, compl_iUnion]
refine fun x ⟨hx₁, hx₂⟩ ↦ mem_iUnion₂.2 ?_
obtain ⟨i, hi⟩ := mem_iUnion.1 <| ht' hx₂
refine ⟨i, ?_, hi⟩
by_contra h
simp only [mem_setOf_eq, not_lt] at h
exact mem_iInter₂.1 hx₁ i h hi
have hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : {k | ν (t' k) < μ (t' k)}), ν (t' n) :=
(measure_mono hcap).trans (measure_biUnion_le ν (to_countable {k | ν (t' k) < μ (t' k)}) _)
refine (add_le_add hle₁ hle₂).trans ?_
have heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ := by ext k; simp [le_or_gt]
conv in ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) => rw [← tsum_univ, ← heq]
rw [ENNReal.summable.tsum_union_disjoint (f := fun n ↦ μ (t' n) ⊓ ν (t' n)) ?_ ENNReal.summable]
· refine add_le_add (tsum_congr ?_).le (tsum_congr ?_).le
· rw [Subtype.forall]
intro n hn; simpa
· rw [Subtype.forall]
intro n hn
rw [mem_setOf_eq] at hn
simp [le_of_lt hn]
· rw [Set.disjoint_iff]
rintro k ⟨hk₁, hk₂⟩
rw [mem_setOf_eq] at hk₁ hk₂
exact False.elim <| hk₂.not_ge hk₁
