English
If f is absolutely continuous on uIcc a b, then f has bounded variation on uIcc a b.
Русский
Если f абсолютно непрерывна на uIcc a b, то f имеет ограниченную вариацию на uIcc a b.
LaTeX
$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{BoundedVariationOn}(f, \mathrm{uIcc}(a,b))$$$
Lean4
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` has bounded variation on `uIcc a b`. -/
theorem boundedVariationOn (hf : AbsolutelyContinuousOnInterval f a b) : BoundedVariationOn f (uIcc a b) := by
-- We may assume wlog that `a ≤ b`.
wlog hab₀ : a ≤ b generalizing a b
· specialize @this b a hf.symm (by linarith)
rwa [uIcc_comm]
rw [uIcc_of_le hab₀]
-- Split the cases `a = b` (which is trivial) and `a < b`.
rcases hab₀.eq_or_lt with rfl | hab
·
simp [BoundedVariationOn]
-- Now remains the case `a < b`.
-- Use the `ε`-`δ` definition of AC to get a `δ > 0` such that whenever a finite set of disjoint
-- intervals `uIoc (a i) (b i)`, `i < n` have total length `< δ` and `a i, b i` are all in
-- `[a, b]`, we have `∑ i ∈ range n, dist (f (a i)) (f (b i)) < 1`.
rw [absolutelyContinuousOnInterval_iff] at hf
obtain ⟨δ, hδ₁, hδ₂⟩ := hf 1 (by linarith)
have hab₁ : 0 < b - a := by
linarith
-- Split `[a, b]` into subintervals `[a + i * δ', a + (i + 1) * δ']` for `i = 0, ..., n`, where
-- `a + (n + 1) * δ' = b` and `δ' < δ`.
obtain ⟨n, hn⟩ := exists_nat_one_div_lt (div_pos hδ₁ hab₁)
set δ' := (b - a) / (n + 1)
have hδ₃ : δ' < δ := by
dsimp only [δ']
convert mul_lt_mul_of_pos_right hn hab₁ using 1 <;> field_simp
have h_mono : Monotone fun (i : ℕ) ↦ a + ↑i * δ' :=
by
apply Monotone.const_add
apply Monotone.mul_const Nat.mono_cast
simp only [δ']
refine div_nonneg ?_ ?_ <;>
linarith
-- The variation of `f` on `[a, b]` is the sum of the variations on these subintervals.
have v_sum :
eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + i * δ') (a + (i + 1) * δ')) :=
by
convert eVariationOn.sum' f (I := fun i ↦ a + i * δ') h_mono |>.symm
· simp
· simp only [Nat.cast_add, Nat.cast_one, δ']; field_simp; abel
·
norm_cast
-- The variation of `f` on any subinterval `[x, y]` of `[a, b]` of length `< δ` is `≤ 1`.
have v_each (x y : ℝ) (_ : a ≤ x) (_ : x ≤ y) (_ : y < x + δ) (_ : y ≤ b) : eVariationOn f (Icc x y) ≤ 1 :=
by
simp only [eVariationOn, iSup_le_iff]
intro p
obtain ⟨hp₁, hp₂⟩ := p.2.property
have vf : ∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) < 1 :=
by
apply hδ₂ (p.1, (fun i ↦ (p.2.val i, p.2.val (i + 1))))
· constructor
· have : Icc x y ⊆ uIcc a b := by rw [uIcc_of_le hab₀]; gcongr
intro i hi
constructor <;> exact this (hp₂ _)
· rw [PairwiseDisjoint]
convert hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1) using 3
rw [uIoc_of_le (hp₁ (by omega))]
rfl
· suffices p.2.val p.1 - p.2.val 0 < δ by
convert this
rw [← Finset.sum_range_sub]
congr; ext i
rw [dist_comm, Real.dist_eq, abs_eq_self.mpr]
linarith [@hp₁ i (i + 1) (by omega)]
linarith [mem_Icc.mp (hp₂ p.1), mem_Icc.mp (hp₂ 0)]
-- Reduce edist in the goal to dist and clear up
have veq :
(∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i))).toReal =
∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) :=
by
rw [ENNReal.toReal_sum (by simp [edist_ne_top])]
simp_rw [← dist_edist]; congr; ext i; nth_rw 1 [dist_comm]
have not_top : ∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i)) ≠ ⊤ := by simp [edist_ne_top]
rw [← ENNReal.ofReal_toReal not_top]
convert ENNReal.ofReal_le_ofReal (veq.symm ▸ vf.le)
simp
-- Reduce to goal that the variation of `f` on each of these subintervals is finite.
simp only [BoundedVariationOn, v_sum, ne_eq, ENNReal.sum_eq_top, Finset.mem_range, not_exists, not_and]
intro i hi
suffices eVariationOn f (Icc (a + i * δ') (a + (i + 1) * δ')) ≤ 1 from fun hC ↦ by simp [hC] at this
apply v_each
· convert h_mono (show 0 ≤ i by omega); simp
· convert h_mono (show i ≤ i + 1 by omega); norm_cast
· rw [add_mul, ← add_assoc]; simpa
· convert h_mono (show i + 1 ≤ n + 1 by omega)
· norm_cast
· simp only [Nat.cast_add, Nat.cast_one, δ']; field_simp; abel
