Chuangjie Xu, 2013

\begin{code}

module UniformContinuity where

open import MiniLibrary
open import Inequality
open import Sequence
open import not-not


constant : {X Y : Set} → (X → Y) → Set
constant {X} {Y} f = ∀(x x' : X) → f x ≡ f x'

Lemma[∘-constant] : {X Y Z : Set} → (f : X → Y) → (g : Y → Z) →
                     constant f → constant (g ∘ f)
Lemma[∘-constant] f g cf x x' = ap g (cf x x')

[constant] : {X Y : Set} → (X → Y) → Set
[constant] {X} {Y} f = ∀(x x' : X) → [ f x ≡ f x' ]

Lemma[∘-[constant]] : {X Y Z : Set} → (f : X → Y) → (g : Y → Z) →
                       [constant] f → [constant] (g ∘ f)
Lemma[∘-[constant]] f g cf x x' = [ap] g (cf x x')

∃-min : (ℕ → Set) → Set
∃-min P = ∃ \(n : ℕ) → (P n) ∧ (∀(n' : ℕ) → P n' → n ≤ n')

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

\end{code}

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

\begin{code}

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

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] P claim n
 where
  P : (n : ℕ) → ₂Fin n → Set
  P n s = p (cons s 0̄) ~ p (cons s 1̄)
  claim : ∀(n : ℕ) → ∀(s : ₂Fin n) → decidable (P n s)
  claim n 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         = 
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 ≡ in₀ h → LM _~_ dec p (succ n) ≡ LM _~_ dec p n
  claim₀ _ r = ap (case _ _) r
  claim₁ : ∀ f → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ in₁ 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 ≡ in₀ h → LM _~_ dec p (succ n) ≡ succ n
  claim₀ h = ∅-elim (f h)
  claim₁ : ∀ f → Lemma[decidable-0̄-1̄] _~_ dec p n ≡ in₁ 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≡₁] (α n))
   where
    sclaim₀ : α n ≡ ₀ → α ≣[ succ n ] cons s 0̄
    sclaim₀ αn₀ = ≣[succ]
                    (Lemma[cons-take-≣[]] n α 0̄) (trans αn₀ (sym (eq0̄ s)))
    sclaim₁ : α n ≡ ₁ → α ≣[ succ n ] cons s 1̄
    sclaim₁ αn₁ = ≣[succ]
                    (Lemma[cons-take-≣[]] n α 1̄) (trans αn₁ (sym (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 {₂Fin n} {λ s → (β ≣[ succ n ] cons s 0̄) ∨ (β ≣[ succ n ] cons s 1̄)}
                    (sym (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̄) (trans βn₀ (sym (eq0̄ s')))
    sclaim₁ : β n ≡ ₁ → β ≣[ succ n ] cons s' 1̄
    sclaim₁ βn₁ = ≣[succ] (Lemma[cons-take-≣[]] n β 1̄) (trans βn₁ (sym (eq1̄ s')))
    sclaim₂ : (β ≣[ succ n ] cons s' 0̄) ∨ (β ≣[ succ n ] cons s' 1̄)
    sclaim₂ = cases sclaim₀ sclaim₁ (Lemma[b≡₀∨b≡₁] (β n))
  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         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         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} (sym 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 =
  ∃-intro (LM _~_ dec p n) (∧-intro (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 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 sym trans


\end{code}

Identity map is uniformly continuous. Function composition preserves
uniform continuity.

\begin{code}

Lemma[id-UC] : uniformly-continuous-₂ℕ id
Lemma[id-UC] m = ∃-intro m (∧-intro 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} (sym (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₀ = ∃-witness (uc₀ m)
  pr₀ : ∀(α β : ₂ℕ) → α ≣[ n₀ ] β → t₀ α ≣[ m ] t₀ β
  pr₀ = ∧-elim₀ (∃-elim (uc₀ m))
  n₁ : ℕ
  n₁ = ∃-witness (uc₁ n₀)
  pr₁ : ∀(α β : ₂ℕ) → α ≣[ n₁ ] β → t₁ α ≣[ n₀ ] t₁ β
  pr₁ = ∧-elim₀ (∃-elim (uc₁ n₀))
  pr : ∀(α β : ₂ℕ) → α ≣[ n₁ ] β → t₀ (t₁ α) ≣[ m ] t₀ (t₁ β)
  pr α β e = (pr₀ (t₁ α) (t₁ β)) (pr₁ α β 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)         = ∃-intro  ((λ _ _ _ → ≣[zero]) , (λ _ _ → ≤-zero))
Lemma[cons-UC] (b ∷ s) (succ m) = ∃-intro n (∧-intro prs mins)
 where
  IH : ∃-min \(n : ℕ) → ∀(α β : ₂ℕ) → α ≣[ n ] β → cons s α ≣[ m ] cons s β
  IH = Lemma[cons-UC] s m
  n : ℕ
  n = ∃-witness IH
  prn : ∀(α β : ₂ℕ) → α ≣[ n ] β → cons s α ≣[ m ] cons s β
  prn = ∧-elim₀ (∃-elim IH)
  claim₀ : ∀(α β : ₂ℕ) → α ≣[ n ] β → cons s α ≣[ m ] cons s β →
            ∀(i : ℕ) → i < succ m → cons (b ∷ s) α i ≡ cons (b ∷ s) β i
  claim₀ α β en em         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 = ∧-elim₁ (∃-elim 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}