length_subadditive_Icc_Ioo — Mathlib

English

If a compact interval [a,b] is covered by a union of open intervals (c_i, d_i), then the Stieltjes length bound holds: ofReal(f(b) - f(a)) ≤ sum' ofReal(f(d_i) - f(c_i)).

Русский

Если компактный отрезок [a,b] покрывается объединением открытых интервалов (c_i, d_i), то выполняется неравенство: ofReal(f(b) - f(a)) ≤ сумма по i от ofReal(f(d_i) - f(c_i)).

LaTeX

$$Icc(a,b) ⊆ ⋃_i Ioo(c_i,d_i) → ofReal(f(b) - f(a)) ≤ ∑' i, ofReal(f(d_i) - f(c_i))$$

Lean4

/-- If a compact interval `[a, b]` is covered by a union of open interval `(c i, d i)`, then
`f b - f a ≤ ∑ f (d i) - f (c i)`. This is an auxiliary technical statement to prove the same
statement for half-open intervals, the point of the current statement being that one can use
compactness to reduce it to a finite sum, and argue by induction on the size of the covering set. -/
theorem length_subadditive_Icc_Ioo {a b : ℝ} {c d : ℕ → ℝ} (ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)) :
    ofReal (f b - f a) ≤ ∑' i, ofReal (f (d i) - f (c i)) :=
  by
  suffices
    ∀ (s : Finset ℕ) (b),
      Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Ioo (c i) (d i)) → (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i ∈ s, ofReal (f (d i) - f (c i))
    by
    rcases
      isCompact_Icc.elim_finite_subcover_image (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Ioo _ _ _ _ (c i) (d i))
        (by simpa using ss) with
      ⟨s, _, hf, hs⟩
    have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i) := by
      simp only [Finset.set_biUnion_coe, Finite.mem_toFinset]
    rw [ENNReal.tsum_eq_iSup_sum]
    refine le_trans ?_ (le_iSup _ hf.toFinset)
    exact this hf.toFinset _ (by simpa only [e])
  clear ss b
  refine fun s => Finset.strongInductionOn s fun s IH b cv => ?_
  rcases le_total b a with ab | ab
  · rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]
    exact zero_le _
  have := cv ⟨ab, le_rfl⟩
  simp only [Finset.mem_coe, mem_iUnion, mem_Ioo, exists_and_left, exists_prop] at this
  rcases this with ⟨i, cb, is, bd⟩
  rw [← Finset.insert_erase is] at cv ⊢
  rw [Finset.coe_insert, biUnion_insert] at cv
  rw [Finset.sum_insert (Finset.notMem_erase _ _)]
  grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le]
  · gcongr
    rw [sub_add_sub_cancel]
    exact sub_le_sub_right (f.mono bd.le) _
  · rintro x ⟨h₁, h₂⟩
    exact (cv ⟨h₁, le_trans h₂ (le_of_lt cb)⟩).resolve_left (mt And.left (not_lt_of_ge h₂))

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