English
Same subadditivity as above but for a finite family of open intervals; if Icc(a,b) is contained in the union of open intervals Ioo(ci, di), then the same bound holds.
Русский
Та же неравенство подаддитивности при конечном покрытии: если Icc(a,b) ⊆ ⋃_i Ioo(ci,di), то выполняется аналогичное неравенство.
LaTeX
$$Icc(a,b) ⊆ ⋃ i, Ioo(ci,di) → ofReal(f(b) - f(a)) ≤ ∑' i, ofReal(f(di) - f(ci))$$
Lean4
@[simp]
theorem outer_Ioc (a b : ℝ) : f.outer (Ioc a b) = ofReal (f b - f a) := by
/- It suffices to show that, if `(a, b]` is covered by sets `s i`, then `f b - f a` is bounded
by `∑ f.length (s i) + ε`. The difficulty is that `f.length` is expressed in terms of half-open
intervals, while we would like to have a compact interval covered by open intervals to use
compactness and finite sums, as provided by `length_subadditive_Icc_Ioo`. The trick is to use
the right-continuity of `f`. If `a'` is close enough to `a` on its right, then `[a', b]` is
still covered by the sets `s i` and moreover `f b - f a'` is very close to `f b - f a`
(up to `ε/2`).
Also, by definition one can cover `s i` by a half-closed interval `(p i, q i]` with `f`-length
very close to that of `s i` (within a suitably small `ε' i`, say). If one moves `q i` very
slightly to the right, then the `f`-length will change very little by right continuity, and we
will get an open interval `(p i, q' i)` covering `s i` with `f (q' i) - f (p i)` within `ε' i`
of the `f`-length of `s i`. -/
refine
le_antisymm
(by
rw [← f.length_Ioc]
apply outer_le_length)
(le_iInf₂ fun s hs => ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_)
let δ := ε / 2
have δpos : 0 < (δ : ℝ≥0∞) := by simpa [δ] using εpos.ne'
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩
obtain ⟨a', ha', aa'⟩ : ∃ a', f a' - f a < δ ∧ a < a' :=
by
have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a :=
by
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
exact (f.right_continuous a).mono Ioi_subset_Ici_self
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists
have : ∀ i, ∃ p : ℝ × ℝ, s i ⊆ Ioo p.1 p.2 ∧ (ofReal (f p.2 - f p.1) : ℝ≥0∞) < f.length (s i) + ε' i :=
by
intro i
have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
conv at hl =>
lhs
rw [length]
simp only [iInf_lt_iff, exists_prop] at hl
rcases hl with ⟨p, q', spq, hq'⟩
have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' :=
by
apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
exact (f.right_continuous q').mono Ioi_subset_Ici_self
rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩
choose g hg using this
have I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2 :=
calc
Icc a' b ⊆ Ioc a b := fun x hx => ⟨aa'.trans_le hx.1, hx.2⟩
_ ⊆ ⋃ i, s i := hs
_ ⊆ ⋃ i, Ioo (g i).1 (g i).2 := iUnion_mono fun i => (hg i).1
calc
ofReal (f b - f a) = ofReal (f b - f a' + (f a' - f a)) := by rw [sub_add_sub_cancel]
_ ≤ ofReal (f b - f a') + ofReal (f a' - f a) := ENNReal.ofReal_add_le
_ ≤ ∑' i, ofReal (f (g i).2 - f (g i).1) + ofReal δ :=
(add_le_add (f.length_subadditive_Icc_Ioo I_subset) (ENNReal.ofReal_le_ofReal ha'.le))
_ ≤ ∑' i, (f.length (s i) + ε' i) + δ :=
(add_le_add (ENNReal.tsum_le_tsum fun i => (hg i).2.le) (by simp only [ENNReal.ofReal_coe_nnreal, le_rfl]))
_ = ∑' i, f.length (s i) + ∑' i, (ε' i : ℝ≥0∞) + δ := by rw [ENNReal.tsum_add]
_ ≤ ∑' i, f.length (s i) + δ + δ := (add_le_add (add_le_add le_rfl hε.le) le_rfl)
_ = ∑' i : ℕ, f.length (s i) + ε := by simp [δ, add_assoc, ENNReal.add_halves]
