Absolutely Continuous Functions

This file defines absolutely continuous functions on a closed interval uIcc a b and proves some basic properties about absolutely continuous functions.

A function f is absolutely continuous on uIcc a b if for any ε > 0, there is δ > 0 such that for any finite disjoint collection of intervals uIoc (a i) (b i) for i < n where a i, b i are all in uIcc a b for i < n, if ∑ i ∈ range n, dist (a i) (b i) < δ, then ∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε.

We give a filter version of the definition of absolutely continuous functions in AbsolutelyContinuousOnInterval based on AbsolutelyContinuousOnInterval.totalLengthFilter and AbsolutelyContinuousOnInterval.disjWithin and prove its equivalence with the ε-δ definition in absolutelyContinuousOnInterval_iff.

We use the filter version to prove that absolutely continuous functions are closed under

• addition - AbsolutelyContinuousOnInterval.fun_add, AbsolutelyContinuousOnInterval.add;
• negation - AbsolutelyContinuousOnInterval.fun_neg, AbsolutelyContinuousOnInterval.neg;
• subtraction - AbsolutelyContinuousOnInterval.fun_sub, AbsolutelyContinuousOnInterval.sub;
• scalar multiplication - AbsolutelyContinuousOnInterval.const_smul, AbsolutelyContinuousOnInterval.const_mul;
• multiplication - AbsolutelyContinuousOnInterval.fun_smul, AbsolutelyContinuousOnInterval.smul, AbsolutelyContinuousOnInterval.fun_mul, AbsolutelyContinuousOnInterval.mul; and that absolutely continuous implies uniform continuous in AbsolutelyContinuousOnInterval.uniformlyContinuousOn

We use the the ε-δ definition to prove that

• Lipschitz continuous functions are absolutely continuous - LipschitzOnWith.absolutelyContinuousOnInterval;
• absolutely continuous functions have bounded variation - AbsolutelyContinuousOnInterval.boundedVariationOn.

Tags

absolutely continuous

def AbsolutelyContinuousOnInterval.totalLengthFilter {X : Type u_1} [PseudoMetricSpace X] : Filter (ℕ × (ℕ → X × X))

The filter on the collection of all the finite sequences of uIoc intervals induced by the function that maps the finite sequence of the intervals to the total length of the intervals. Details:

1. Technically the filter is on ℕ × (ℕ → X × X). A finite sequence uIoc (a i) (b i), i < n is represented by any E : ℕ × (ℕ → X × X) which satisfies E.1 = n and E.2 i = (a i, b i) for i < n. Its total length is ∑ i ∈ Finset.range n, dist (a i) (b i).
2. For a sequence G : ℕ → ℕ × (ℕ → X × X), G convergence along totalLengthFilter means that the total length of G j, i.e., ∑ i ∈ Finset.range (G j).1, dist ((G j).2 i).1 ((G j).2 i).2), tends to 0 as j tends to infinity.

Equations

• AbsolutelyContinuousOnInterval.totalLengthFilter = Filter.comap (fun (E : ℕ × (ℕ → X × X)) => ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (nhds 0)

theorem AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter {X : Type u_1} [PseudoMetricSpace X] : totalLengthFilter.HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}

def AbsolutelyContinuousOnInterval.disjWithin (a b : ℝ) : Set (ℕ × (ℕ → ℝ × ℝ))

The subcollection of all the finite sequences of uIoc intervals consisting of uIoc (a i) (b i), i < n where a i, b i are all in uIcc a b for i < n and uIoc (a i) (b i) are mutually disjoint for i < n. Technically the finite sequence uIoc (a i) (b i), i < n is represented by any E : ℕ × (ℕ → ℝ × ℝ) which satisfies E.1 = n and E.2 i = (a i, b i) for i < n.

Equations

• One or more equations did not get rendered due to their size.

theorem AbsolutelyContinuousOnInterval.disjWithin_comm (a b : ℝ) : disjWithin a b = disjWithin b a

theorem AbsolutelyContinuousOnInterval.disjWithin_mono {a b c d : ℝ} (habcd : Set.uIcc c d ⊆ Set.uIcc a b) : disjWithin c d ⊆ disjWithin a b

def AbsolutelyContinuousOnInterval {X : Type u_1} [PseudoMetricSpace X] (f : ℝ → X) (a b : ℝ) : Prop

AbsolutelyContinuousOnInterval f a b: A function f is absolutely continuous on uIcc a b if the function which (intuitively) maps uIoc (a i) (b i), i < n to ∑ i ∈ Finset.range n, dist (f (a i)) (f (b i)) tendsto 𝓝 0 wrt totalLengthFilter restricted to disjWithin a b. This is equivalent to the traditional ε-δ definition: for any ε > 0, there is δ > 0 such that for any finite disjoint collection of intervals uIoc (a i) (b i) for i < n where a i, b i are all in uIcc a b for i < n, if ∑ i ∈ range n, dist (a i) (b i) < δ, then ∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε.

Equations

• One or more equations did not get rendered due to their size.

theorem absolutelyContinuousOnInterval_iff {X : Type u_1} [PseudoMetricSpace X] (f : ℝ → X) (a b : ℝ) : AbsolutelyContinuousOnInterval f a b ↔ ∀ ε > 0, ∃ δ > 0, ∀ E ∈ AbsolutelyContinuousOnInterval.disjWithin a b, ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε

The traditional ε-δ definition of absolutely continuous: A function f is absolutely continuous on uIcc a b if for any ε > 0, there is δ > 0 such that for any finite disjoint collection of intervals uIoc (a i) (b i) for i < n where a i, b i are all in uIcc a b for i < n, if ∑ i ∈ range n, dist (a i) (b i) < δ, then ∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε.

theorem AbsolutelyContinuousOnInterval.symm {X : Type u_1} [PseudoMetricSpace X] {f : ℝ → X} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval f b a

theorem AbsolutelyContinuousOnInterval.mono {X : Type u_1} [PseudoMetricSpace X] {f : ℝ → X} {a b c d : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (habcd : Set.uIcc c d ⊆ Set.uIcc a b) : AbsolutelyContinuousOnInterval f c d

theorem AbsolutelyContinuousOnInterval.fun_add {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => f x + g x) a b

theorem AbsolutelyContinuousOnInterval.add {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (f + g) a b

theorem AbsolutelyContinuousOnInterval.fun_neg {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => -f x) a b

theorem AbsolutelyContinuousOnInterval.neg {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (-f) a b

theorem AbsolutelyContinuousOnInterval.fun_sub {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => f x - g x) a b

theorem AbsolutelyContinuousOnInterval.sub {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (f - g) a b

theorem AbsolutelyContinuousOnInterval.const_smul {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} {M : Type u_3} [SeminormedRing M] [Module M F] [NormSMulClass M F] (α : M) (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => α • f x) a b

theorem AbsolutelyContinuousOnInterval.const_mul {a b : ℝ} {f : ℝ → ℝ} (α : ℝ) (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => α * f x) a b

theorem AbsolutelyContinuousOnInterval.uniformity_eq_comap_totalLengthFilter {X : Type u_1} [PseudoMetricSpace X] : uniformity X = Filter.comap (fun (x : X × X) => (1, fun (x_1 : ℕ) => x)) totalLengthFilter

theorem AbsolutelyContinuousOnInterval.uniformlyContinuousOn {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : UniformContinuousOn f (Set.uIcc a b)

If f is absolutely continuous on uIcc a b, then f is uniformly continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.continuousOn {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : ContinuousOn f (Set.uIcc a b)

If f is absolutely continuous on uIcc a b, then f is continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.exists_bound {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : ∃ (C : ℝ), ∀ x ∈ Set.uIcc a b, ‖f x‖ ≤ C

If f is absolutely continuous on uIcc a b, then f is bounded on uIcc a b.

theorem AbsolutelyContinuousOnInterval.fun_smul {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {M : Type u_3} [SeminormedRing M] [Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => f x • g x) a b

If f and g are absolutely continuous on uIcc a b, then f • g is absolutely continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.smul {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {M : Type u_3} [SeminormedRing M] [Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (f • g) a b

If f and g are absolutely continuous on uIcc a b, then f • g is absolutely continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.fun_mul {a b : ℝ} {f g : ℝ → ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => f x * g x) a b

If f and g are absolutely continuous on uIcc a b, then f * g is absolutely continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.mul {a b : ℝ} {f g : ℝ → ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (x : ℝ) => f x * g x) a b

If f and g are absolutely continuous on uIcc a b, then f * g is absolutely continuous on uIcc a b.

theorem LipschitzOnWith.absolutelyContinuousOnInterval {X : Type u_1} [PseudoMetricSpace X] {a b : ℝ} {f : ℝ → X} {K : NNReal} (hfK : LipschitzOnWith K f (Set.uIcc a b)) : AbsolutelyContinuousOnInterval f a b

If f is Lipschitz on uIcc a b, then f is absolutely continuous on uIcc a b.

theorem AbsolutelyContinuousOnInterval.boundedVariationOn {F : Type u_2} [SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F} (hf : AbsolutelyContinuousOnInterval f a b) : BoundedVariationOn f (Set.uIcc a b)

If f is absolutely continuous on uIcc a b, then f has bounded variation on uIcc a b.