Chuangjie Xu 2013

\begin{code}

{-# OPTIONS --without-K #-}

module Continuity.UniformContinuity where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Preliminaries.Boolean
open import Preliminaries.Sequence

\end{code}

In the definitions of local constancy and uniform continuity, we require the
moduli to be the minimal.

\begin{code}

locally-constant : {X : Set} → (₂ℕ → X) → Set
locally-constant p = Σ-min \(n : ℕ) → ∀(α β : ₂ℕ) → α ≡[ n ] β → p α ≡ p β

Axiom[UC-ℕ] : Set
Axiom[UC-ℕ] = ∀(f : ₂ℕ → ℕ) → locally-constant f

uniformly-continuous-₂ℕ : (₂ℕ → ₂ℕ) → Set
uniformly-continuous-₂ℕ t = ∀(m : ℕ) → Σ-min \(n : ℕ) → ∀(α β : ₂ℕ) → α ≡[ n ] β → t α ≡[ m ] t β

\end{code}

Here we provide an algorithm to compute least moduli of uniform continuity.

\begin{code}

Lemma[decidable-0̄-1̄] : {X : Set} → (_~_ : X → X → Set) →
(∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
(p : ₂ℕ → X) → (n : ℕ) →
decidable (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄))
Lemma[decidable-0̄-1̄] _~_ dec p n = Lemma[₂Fin-decidability] n P claim
where
P : ₂Fin n → Set
P s = p (cons s 0̄) ~ p (cons s 1̄)
claim : ∀(s : ₂Fin n) → decidable (P s)
claim s = dec (p (cons s 0̄)) (p (cons s 1̄))

LM : {X : Set} → (_~_ : X → X → Set) → (∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
(₂ℕ → X) → ℕ → ℕ
LM _~_ dec p 0        = 0
LM _~_ dec p (succ n) = case f₀ f₁ (Lemma[decidable-0̄-1̄] _~_ dec p n)
where
f₀ : (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) → ℕ
f₀ _ = LM _~_ dec p n
f₁ : ¬ (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) → ℕ
f₁ _ = succ n

LM-₂ℕ : {m : ℕ} → (₂ℕ → ₂ℕ) → ℕ → ℕ
LM-₂ℕ {m} = LM {₂ℕ} (λ α β → α ≡[ m ] β) Lemma[≡[]-decidable]

LM-ℕ : (₂ℕ → ℕ) → ℕ → ℕ
LM-ℕ = LM {ℕ} _≡_ ℕ-discrete

LM-₂ : (₂ℕ → ₂) → ℕ → ℕ
LM-₂ = LM {₂} _≡_ ₂-discrete

Lemma[LM]₀ : {X : Set} → (_~_ : X → X → Set) → (dec : ∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
(p : ₂ℕ → X) → (n : ℕ) →
(∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) →
LM _~_ dec p (succ n) ≡ LM _~_ dec p n
Lemma[LM]₀ _~_ dec p n h = equality-cases (Lemma[decidable-0̄-1̄] _~_ dec p n) claim₀ claim₁
where
claim₀ : ∀ h → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ inl h → LM _~_ dec p (succ n) ≡ LM _~_ dec p n
claim₀ _ r = ap (case _ _) r
claim₁ : ∀ f → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ inr f → LM _~_ dec p (succ n) ≡ LM _~_ dec p n
claim₁ f = ∅-elim(f h)

Lemma[LM]₁ : {X : Set} → (_~_ : X → X → Set) → (dec : ∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
(p : ₂ℕ → X) → (n : ℕ) →
¬ (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) →
LM _~_ dec p (succ n) ≡ succ n
Lemma[LM]₁ _~_ dec p n f = equality-cases (Lemma[decidable-0̄-1̄] _~_ dec p n) claim₀ claim₁
where
claim₀ : ∀ h → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ inl h → LM _~_ dec p (succ n) ≡ succ n
claim₀ h = ∅-elim (f h)
claim₁ : ∀ f → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ inr f → LM _~_ dec p (succ n) ≡ succ n
claim₁ _ r = ap (case _ _) r

Lemma[succ-0̄-1̄] : {X : Set} → (_~_ : X → X → Set) →
(∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
({x₀ x₁ : X} → x₀ ~ x₁ → x₁ ~ x₀) →
({x₀ x₁ x₂ : X} → x₀ ~ x₁ → x₁ ~ x₂ → x₀ ~ x₂) →
(p : ₂ℕ → X) → (n : ℕ) →
(∀(α β : ₂ℕ) → α ≡[ succ n ] β → p α ~ p β) →
(∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) →
∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β
Lemma[succ-0̄-1̄] {X} _~_ dec sy tr p n pr g α β en = tr eqα (sy eqβ)
where
s : ₂Fin n
s = take n α
eq : p (cons s 0̄) ~ p (cons s 1̄)
eq = g s
eq0̄ : ∀{k : ℕ} → ∀(t : ₂Fin k) → cons t 0̄ k ≡ ₀
eq0̄ ⟨⟩ = refl
eq0̄ (b ∷ s) = eq0̄ s
eq1̄ : ∀{k : ℕ} → ∀(t : ₂Fin k) → cons t 1̄ k ≡ ₁
eq1̄ ⟨⟩ = refl
eq1̄ (b ∷ s) = eq1̄ s
subclaim₀ : α ≡[ succ n ] cons s 0̄ → p α ~ p (cons s 0̄)
subclaim₀ = pr α (cons s 0̄)
subclaim₁ : α ≡[ succ n ] cons s 1̄ → p α ~ p (cons s 0̄)
subclaim₁ en' = tr (pr α (cons s 1̄) en') (sy eq)
subclaim₂ : (α ≡[ succ n ] cons s 0̄) + (α ≡[ succ n ] cons s 1̄)
subclaim₂ = cases sclaim₀ sclaim₁ Lemma[b≡₀∨b≡₁]
where
sclaim₀ : α n ≡ ₀ → α ≡[ succ n ] cons s 0̄
sclaim₀ αn₀ = ≡[succ] (Lemma[cons-take-≡[]] n α 0̄) (αn₀ · (eq0̄ s)⁻¹)
sclaim₁ : α n ≡ ₁ → α ≡[ succ n ] cons s 1̄
sclaim₁ αn₁ = ≡[succ] (Lemma[cons-take-≡[]] n α 1̄) (αn₁ · (eq1̄ s)⁻¹)
eqα : p α ~ p (cons s 0̄)
eqα = case subclaim₀ subclaim₁ subclaim₂
subclaim₃ : β ≡[ succ n ] cons s 0̄ → p β ~ p (cons s 0̄)
subclaim₃ = pr β (cons s 0̄)
subclaim₄ : β ≡[ succ n ] cons s 1̄ → p β ~ p (cons s 0̄)
subclaim₄ aw' = tr (pr β (cons s 1̄) aw') (sy eq)
subclaim₅ : (β ≡[ succ n ] cons s 0̄) + (β ≡[ succ n ] cons s 1̄)
subclaim₅ = transport (λ s → (β ≡[ succ n ] cons s 0̄) + (β ≡[ succ n ] cons s 1̄))
((Lemma[≡[]-take] en)⁻¹) sclaim₂
where
s' : ₂Fin n
s' = take n β
sclaim₀ : β n ≡ ₀ → β ≡[ succ n ] cons s' 0̄
sclaim₀ βn₀ = ≡[succ] (Lemma[cons-take-≡[]] n β 0̄) (βn₀ · (eq0̄ s')⁻¹)
sclaim₁ : β n ≡ ₁ → β ≡[ succ n ] cons s' 1̄
sclaim₁ βn₁ = ≡[succ] (Lemma[cons-take-≡[]] n β 1̄) (βn₁ · (eq1̄ s')⁻¹)
sclaim₂ : (β ≡[ succ n ] cons s' 0̄) + (β ≡[ succ n ] cons s' 1̄)
sclaim₂ = cases sclaim₀ sclaim₁ Lemma[b≡₀∨b≡₁]
eqβ : p β ~ p (cons s 0̄)
eqβ = case subclaim₃ subclaim₄ subclaim₅

Lemma[LM-modulus] : {X : Set} → (_~_ : X → X → Set) →
(dec : ∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
({x₀ x₁ : X} → x₀ ~ x₁ → x₁ ~ x₀) →
({x₀ x₁ x₂ : X} → x₀ ~ x₁ → x₁ ~ x₂ → x₀ ~ x₂) →
(p : ₂ℕ → X) → (n : ℕ) →
(∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β) →
∀(α β : ₂ℕ) → α ≡[ LM _~_ dec p n ] β → p α ~ p β
Lemma[LM-modulus] _~_ dec sy tr p 0        pr α β e = pr α β e
Lemma[LM-modulus] _~_ dec sy tr p (succ n) pr α β e =
case claim₀ claim₁ (Lemma[decidable-0̄-1̄] _~_ dec p n)
where
claim₀ : (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) → p α ~ p β
claim₀ h = Lemma[LM-modulus] _~_ dec sy tr p n pr' α β e'
where
fact : LM _~_ dec p (succ n) ≡ LM _~_ dec p n
fact = Lemma[LM]₀ _~_ dec p n h
e' : α ≡[ LM _~_ dec p n ] β
e' = transport (λ k → α ≡[ k ] β) fact e
pr' : ∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β
pr' = Lemma[succ-0̄-1̄] _~_ dec sy tr p n pr h
claim₁ : ¬ (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) → p α ~ p β
claim₁ f = pr α β e'
where
fact : LM _~_ dec p (succ n) ≡ succ n
fact = Lemma[LM]₁ _~_ dec p n f
e' : α ≡[ succ n ] β
e' = transport (λ k → α ≡[ k ] β) fact e

Lemma[LM-least] : {X : Set} → (_~_ : X → X → Set) →
(dec : ∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
({x₀ x₁ : X} → x₀ ~ x₁ → x₁ ~ x₀) →
({x₀ x₁ x₂ : X} → x₀ ~ x₁ → x₁ ~ x₂ → x₀ ~ x₂) →
(p : ₂ℕ → X) →
(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β) →
(k : ℕ) → (∀(α β : ₂ℕ) → α ≡[ k ] β → p α ~ p β) →
LM _~_ dec p n ≤ k
Lemma[LM-least] _~_ dec sy tr p 0        prn k prk = ≤-zero
Lemma[LM-least] _~_ dec sy tr p (succ n) prn k prk = case claim₀ claim₁ claim₂
where
claim₀ : (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) →
LM _~_ dec p (succ n) ≤ k
claim₀ h = transport (λ l → l ≤ k) (fact ⁻¹) IH
where
fact : LM _~_ dec p (succ n) ≡ LM _~_ dec p n
fact = Lemma[LM]₀ _~_ dec p n h
prn' : ∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β
prn' = Lemma[succ-0̄-1̄] _~_ dec sy tr p n prn h
IH : LM _~_ dec p n ≤ k
IH = Lemma[LM-least] _~_ dec sy tr p n prn' k prk
claim₁ : ¬ (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)) →
LM _~_ dec p (succ n)  ≤ k
claim₁ f = Lemma[m≮n→n≤m] goal
where
fact : LM _~_ dec p (succ n) ≡ succ n
fact = Lemma[LM]₁ _~_ dec p n f
goal : k ≮ LM _~_ dec p (succ n)
goal r = f c₃
where
c₀ : k < succ n
c₀ = transport (λ l → k < l) fact r
c₁ : k ≤ n
c₁ = Lemma[m+1≤n+1→m≤n] c₀
c₂ : ∀(s : ₂Fin n) → (cons s 0̄) ≡[ k ] (cons s 1̄)
c₂ s = Lemma[≡[]-≤] (Lemma[cons-≡[]] s 0̄ 1̄) c₁
c₃ : ∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄)
c₃ s = prk (cons s 0̄) (cons s 1̄) (c₂ s)
claim₂ : decidable (∀(s : ₂Fin n) → p (cons s 0̄) ~ p (cons s 1̄))
claim₂ = Lemma[decidable-0̄-1̄] _~_ dec p n

Lemma[LM-least-modulus] : {X : Set} → (_~_ : X → X → Set) →
(dec : ∀(x₀ x₁ : X) → decidable (x₀ ~ x₁)) →
({x₀ x₁ : X} → x₀ ~ x₁ → x₁ ~ x₀) →
({x₀ x₁ x₂ : X} → x₀ ~ x₁ → x₁ ~ x₂ → x₀ ~ x₂) →
(p : ₂ℕ → X) →
(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → p α ~ p β) →
Σ-min \(k : ℕ) → (∀(α β : ₂ℕ) → α ≡[ k ] β → p α ~ p β)
Lemma[LM-least-modulus] _~_ dec sy tr p n pr =
(LM _~_ dec p n) , (Lemma[LM-modulus] _~_ dec sy tr p n pr) , (Lemma[LM-least] _~_ dec sy tr p n pr)

Lemma[LM-₂ℕ-least-modulus] : {m : ℕ} → ∀(t : ₂ℕ → ₂ℕ) →
(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → t α ≡[ m ] t β) →
Σ-min \(k : ℕ) → ∀(α β : ₂ℕ) → α ≡[ k ] β → t α ≡[ m ] t β
Lemma[LM-₂ℕ-least-modulus] {m} = Lemma[LM-least-modulus] (λ α β → α ≡[ m ] β) Lemma[≡[]-decidable] ≡[]-sym ≡[]-trans

Lemma[LM-ℕ-least-modulus] : ∀(p : ₂ℕ → ℕ) →
(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → p α ≡ p β) →
Σ-min \(k : ℕ) → ∀(α β : ₂ℕ) → α ≡[ k ] β → p α ≡ p β
Lemma[LM-ℕ-least-modulus] = Lemma[LM-least-modulus] _≡_ ℕ-discrete _⁻¹ _·_

Lemma[LM-₂-least-modulus] : ∀(p : ₂ℕ → ₂) →
(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → p α ≡ p β) →
Σ-min \(k : ℕ) → ∀(α β : ₂ℕ) → α ≡[ k ] β → p α ≡ p β
Lemma[LM-₂-least-modulus] = Lemma[LM-least-modulus] _≡_ ₂-discrete _⁻¹ _·_

\end{code}

Identity map is uniformly continuous.

Function composition preserves uniform continuity.

Concatenation maps are uniformly continuous.

\begin{code}

Lemma[id-UC] : uniformly-continuous-₂ℕ id
Lemma[id-UC] m = m , prp , min
where
prp : ∀(α β : ₂ℕ) → α ≡[ m ] β → id α ≡[ m ] id β
prp α β em = em
min : ∀(n : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n ] β → id α ≡[ m ] id β) → m ≤ n
min n prn = Lemma[m≮n→n≤m] claim
where
claim : n ≮ m
claim r = c₃ c₂
where
α : ₂ℕ
α = 0̄
β : ₂ℕ
β = overwrite 0̄ n ₁
c₀ : α ≡[ n ] β
c₀ = Lemma[overwrite-≡[]] 0̄ n ₁
c₁ : α ≡[ succ n ] β
c₁ = Lemma[≡[]-≤] (prn α β c₀) r
c₂ : α n ≡ β n
c₂ = Lemma[≡[succ]]₁ c₁
c₃ : α n ≠ β n
c₃ = transport (λ b → ₀ ≠ b) ((Lemma[overwrite] 0̄ n ₁)⁻¹) Lemma[₀≠₁]

Lemma[∘-UC] : ∀(t₀ : ₂ℕ → ₂ℕ) → uniformly-continuous-₂ℕ t₀ →
∀(t₁ : ₂ℕ → ₂ℕ) → uniformly-continuous-₂ℕ t₁ →
uniformly-continuous-₂ℕ (t₀ ∘ t₁)
Lemma[∘-UC] t₀ uc₀ t₁ uc₁ m = Lemma[LM-₂ℕ-least-modulus] (t₀ ∘ t₁) n₁ pr
where
n₀ : ℕ
n₀ = pr₁ (uc₀ m)
prf₀ : ∀(α β : ₂ℕ) → α ≡[ n₀ ] β → t₀ α ≡[ m ] t₀ β
prf₀ = pr₁ (pr₂ (uc₀ m))
n₁ : ℕ
n₁ = pr₁ (uc₁ n₀)
prf₁ : ∀(α β : ₂ℕ) → α ≡[ n₁ ] β → t₁ α ≡[ n₀ ] t₁ β
prf₁ = pr₁ (pr₂ (uc₁ n₀))
pr : ∀(α β : ₂ℕ) → α ≡[ n₁ ] β → t₀ (t₁ α) ≡[ m ] t₀ (t₁ β)
pr α β e = (prf₀ (t₁ α) (t₁ β)) (prf₁ α β e)

Lemma[cons-UC] : ∀{n : ℕ} → ∀(s : ₂Fin n) → uniformly-continuous-₂ℕ (cons s)
Lemma[cons-UC] ⟨⟩      m        = Lemma[id-UC] m
Lemma[cons-UC] (b ∷ s) 0        = 0 , (λ _ _ _ → ≡[zero]) , (λ _ _ → ≤-zero)
Lemma[cons-UC] (b ∷ s) (succ m) = n , prs , mins
where
IH : Σ-min \(n : ℕ) → ∀(α β : ₂ℕ) → α ≡[ n ] β → cons s α ≡[ m ] cons s β
IH = Lemma[cons-UC] s m
n : ℕ
n = pr₁ IH
prn : ∀(α β : ₂ℕ) → α ≡[ n ] β → cons s α ≡[ m ] cons s β
prn = pr₁ (pr₂ IH)
claim₀ : ∀(α β : ₂ℕ) → α ≡[ n ] β → cons s α ≡[ m ] cons s β →
∀(i : ℕ) → i < succ m → cons (b ∷ s) α i ≡ cons (b ∷ s) β i
claim₀ α β en em 0        r          = refl
claim₀ α β en em (succ i) (≤-succ r) = Lemma[≡[]-<] em i r
claim₁ : ∀(α β : ₂ℕ) → α ≡[ n ] β → cons s α ≡[ m ] cons s β →
cons (b ∷ s) α ≡[ succ m ] cons (b ∷ s) β
claim₁ α β en em = Lemma[<-≡[]] (claim₀ α β en em)
prs : ∀(α β : ₂ℕ) → α ≡[ n ] β → cons (b ∷ s) α ≡[ succ m ] cons (b ∷ s) β
prs α β en = claim₁ α β en (prn α β en)
min : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → cons s α ≡[ m ] cons s β) → n ≤ n'
min = pr₂ (pr₂ IH)
lemma : ∀{n m : ℕ}{b : ₂}{s : ₂Fin n}{α β : ₂ℕ} →
cons (b ∷ s) α ≡[ succ m ] cons (b ∷ s) β → cons s α ≡[ m ] cons s β
lemma {n} {m} {b} {s} {α} {β} esm = Lemma[<-≡[]] em'
where
esm' : ∀(i : ℕ) → i < succ m → cons (b ∷ s) α i ≡ cons (b ∷ s) β i
esm' = Lemma[≡[]-<] esm
em' : ∀(i : ℕ) → i < m → cons s α i ≡ cons s β i
em' i r = esm' (succ i) (≤-succ r)
mins : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → cons (b ∷ s) α ≡[ succ m ] cons (b ∷ s) β) → n ≤ n'
mins n' pr' = min n' (λ α β en → lemma (pr' α β en))

\end{code}