Limit approximations and their moduli

A sequence of total functions f : ℕ → α → β, read as the stages f s, converges to g : α → β when it agrees with g at every point from some stage on: ∀ x, ∀ᶠ s in atTop, f s x = g x. The stage after which the value at x is correct depends on x and is not part of the data. A modulus of convergence is a function m : α → ℕ supplying such stages: f s x = g x whenever m x ≤ s.

These are the notions of the Limit Lemma, by which the functions computable relative to the halting problem are exactly the limits of uniformly computable sequences, and of the Modulus Lemma, by which a function computable in a c.e. set has a computable approximation with a modulus computable in that set. Neither lemma is proved here. What is proved is the elementary calculus of limits and moduli, and the unrelativized fact that a uniformly computable sequence with a computable modulus has a computable limit. Convergence alone does not suffice: the halting problem is the limit of its increasing approximation by step-bounded evaluation, which therefore has no computable modulus.

Main definitions

• TauCeti.Approximation.Converges f g: the stages f s agree with g at every point from some stage on.
• TauCeti.Approximation.IsModulus f g m: m x is a stage after which f s x = g x.

Main results

• TauCeti.Approximation.converges_iff_exists_isModulus: a sequence converges exactly when it has a modulus.
• TauCeti.Approximation.Converges.unique: limits are unique.
• TauCeti.Approximation.Converges.eventually_forall_mem, TauCeti.Approximation.IsModulus.forall_mem_of_sup_le: finite-coordinate aggregation. Finitely many coordinates are simultaneously correct from some stage on, and from the largest of their moduli on.
• TauCeti.Approximation.Converges.exists_monotone_isModulus: a convergent sequence on ℕ, or on any locally finite order with a bottom, has a monotone modulus.
• TauCeti.Approximation.converges_shift_iff, TauCeti.Approximation.IsModulus.shift, TauCeti.Approximation.IsModulus.of_shift: shifting the stages preserves the limit, and moves the modulus by the shift.
• TauCeti.Approximation.Converges.comp_tendsto, TauCeti.Approximation.IsModulus.comp: reindexing the stages by a clock tending to infinity preserves the limit; a modulus for the clock turns a modulus of the sequence into one of the reindexed sequence.
• TauCeti.Approximation.IsModulus.computable: a uniformly computable sequence with a computable modulus has a computable limit.
• TauCeti.Approximation.computable_iff_exists_isModulus: a function is computable exactly when it is the limit of a uniformly computable sequence with a computable modulus.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter III.3.

Convergence

def TauCeti.Approximation.Converges {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (g : α → β) : Prop

The stages f s converge to g: at every point x, the value f s x equals g x from some stage on. The stage may depend on x.

theorem TauCeti.Approximation.converges_iff_eventually {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} : Converges f g ↔ ∀ (x : α), ∀ᶠ (s : ℕ) in Filter.atTop, f s x = g x

Unfolding TauCeti.Approximation.Converges.

theorem TauCeti.Approximation.converges_iff_forall_exists {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} : Converges f g ↔ ∀ (x : α), ∃ (s₀ : ℕ), ∀ (s : ℕ), s₀ ≤ s → f s x = g x

Convergence with an explicit stage at every point.

theorem TauCeti.Approximation.converges_iff_tendsto {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} : Converges f g ↔ ∀ (x : α), Filter.Tendsto (fun (s : ℕ) => f s x) Filter.atTop (pure (g x))

Convergence is pointwise convergence to g in the discrete sense: each sequence of values tends to the principal filter of its limit.

theorem TauCeti.Approximation.Converges.unique {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g g' : α → β} (h : Converges f g) (h' : Converges f g') : g = g'

Uniqueness of limits.

theorem TauCeti.Approximation.Converges.apply_eq_of_forall_le {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} (h : Converges f g) {x : α} {s : ℕ} (hs : ∀ (t : ℕ), s ≤ t → f t x = f s x) : f s x = g x

If the value at x no longer changes from stage s on, it is the limit at x.

@[simp]

theorem TauCeti.Approximation.converges_const {α : Type u_1} {β : Type u_2} (g : α → β) : Converges (fun (x : ℕ) => g) g

A constant sequence converges to its value.

theorem TauCeti.Approximation.Converges.eventually_forall_mem {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} (h : Converges f g) (F : Finset α) : ∀ᶠ (s : ℕ) in Filter.atTop, ∀ x ∈ F, f s x = g x

Finite-coordinate aggregation. Finitely many coordinates of a convergent sequence are simultaneously correct from some stage on.

Moduli

def TauCeti.Approximation.IsModulus {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (g : α → β) (m : α → ℕ) : Prop

m is a modulus of the convergence of f to g: from stage m x on, the value at x is g x.

theorem TauCeti.Approximation.isModulus_iff {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} : IsModulus f g m ↔ ∀ (x : α) (s : ℕ), m x ≤ s → f s x = g x

Unfolding TauCeti.Approximation.IsModulus.

theorem TauCeti.Approximation.IsModulus.apply_eq {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} (hm : IsModulus f g m) (x : α) : f (m x) x = g x

The value at the stage given by a modulus is the limit.

theorem TauCeti.Approximation.IsModulus.converges {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} (hm : IsModulus f g m) : Converges f g

A sequence with a modulus converges.

theorem TauCeti.Approximation.converges_iff_exists_isModulus {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} : Converges f g ↔ ∃ (m : α → ℕ), IsModulus f g m

A sequence converges exactly when it has a modulus.

theorem TauCeti.Approximation.Converges.exists_isModulus {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} (h : Converges f g) : ∃ (m : α → ℕ), IsModulus f g m

A convergent sequence has a modulus.

theorem TauCeti.Approximation.IsModulus.mono {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m m' : α → ℕ} (hm : IsModulus f g m) (h : m ≤ m') : IsModulus f g m'

Every larger function is a modulus too.

@[simp]

theorem TauCeti.Approximation.isModulus_const {α : Type u_1} {β : Type u_2} (g : α → β) (m : α → ℕ) : IsModulus (fun (x : ℕ) => g) g m

Every function is a modulus of a constant sequence.

theorem TauCeti.Approximation.IsModulus.forall_mem_of_sup_le {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} (hm : IsModulus f g m) {F : Finset α} {s : ℕ} (hs : F.sup m ≤ s) (x : α) : x ∈ F → f s x = g x

Finite-coordinate aggregation for a modulus. From the largest modulus of finitely many coordinates on, all of them are correct.

theorem TauCeti.Approximation.IsModulus.partialSups {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} [Preorder α] [LocallyFiniteOrderBot α] (hm : IsModulus f g m) : IsModulus f g ⇑(_root_.partialSups m)

A modulus can be replaced by its partial suprema x ↦ max_{y ≤ x} m y, which are monotone (partialSups_monotone). From that stage on, every coordinate up to x is correct.

theorem TauCeti.Approximation.Converges.exists_monotone_isModulus {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} [Preorder α] [LocallyFiniteOrderBot α] (h : Converges f g) : ∃ (m : α → ℕ), Monotone m ∧ IsModulus f g m

A convergent sequence on a locally finite order with a bottom, such as ℕ, has a monotone modulus.

Shifts and reindexing

@[simp]

theorem TauCeti.Approximation.converges_shift_iff {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} (k : ℕ) : Converges (fun (s : ℕ) => f (s + k)) g ↔ Converges f g

Stage shifts. Dropping the first k stages does not change convergence or the limit.

theorem TauCeti.Approximation.IsModulus.shift {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} (hm : IsModulus f g m) (k : ℕ) : IsModulus (fun (s : ℕ) => f (s + k)) g fun (x : α) => m x - k

After dropping the first k stages, a modulus decreases by k.

theorem TauCeti.Approximation.IsModulus.of_shift {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} {k : ℕ} (hm : IsModulus (fun (s : ℕ) => f (s + k)) g m) : IsModulus f g fun (x : α) => m x + k

A modulus of the sequence with the first k stages dropped, increased by k, is a modulus of the original sequence.

theorem TauCeti.Approximation.Converges.comp_tendsto {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} (h : Converges f g) {t : ℕ → ℕ} (ht : Filter.Tendsto t Filter.atTop Filter.atTop) : Converges (fun (s : ℕ) => f (t s)) g

Reindexing by a clock. Reading the stages along a clock t tending to infinity preserves the limit. The clock need not be monotone.

theorem TauCeti.Approximation.IsModulus.comp {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} (hm : IsModulus f g m) {t n : ℕ → ℕ} (ht : ∀ (k s : ℕ), n k ≤ s → k ≤ t s) : IsModulus (fun (s : ℕ) => f (t s)) g fun (x : α) => n (m x)

Effective reindexing. If n k is a stage after which the clock t stays at least k, then n ∘ m is a modulus of the reindexed sequence. For a computable clock modulus n and a computable modulus m, this modulus is computable.

Computability of limits

theorem TauCeti.Approximation.IsModulus.computable {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {g : α → β} {m : α → ℕ} [Primcodable α] [Primcodable β] (hm : IsModulus f g m) (hf : Computable₂ f) (hmc : Computable m) : Computable g

Computable modulus, computable limit. A uniformly computable sequence with a computable modulus has a computable limit: evaluate the sequence at the stage given by the modulus.

theorem TauCeti.Approximation.computable_iff_exists_isModulus {α : Type u_1} {β : Type u_2} {g : α → β} [Primcodable α] [Primcodable β] : Computable g ↔ ∃ (f : ℕ → α → β) (m : α → ℕ), Computable₂ f ∧ Computable m ∧ IsModulus f g m

A function is computable exactly when it is the limit of a uniformly computable sequence with a computable modulus.