UniformContinuity
Chuangjie Xu 2013, ported to TypeTopology in 2025{-# OPTIONS --safe --without-K #-} module C-Spaces.UniformContinuity where open import MLTT.Spartan renaming (_+_ to _⊎_) open import MLTT.Plus-Properties open import MLTT.Two-Properties open import Naturals.Addition open import Naturals.Properties open import UF.DiscreteAndSeparated open import C-Spaces.Preliminaries.Naturals.Order open import C-Spaces.Preliminaries.SequenceIn the definitions of local constancy and uniform continuity, we require the moduli to be minimal.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 βHere we provide an algorithm to compute least moduli of uniform continuity.Lemma[decidable-0̄-1̄] : {X : Set} → (_~_ : X → X → Set) → (∀(x₀ x₁ : X) → is-decidable (x₀ ~ x₁)) → (p : ₂ℕ → X) → (n : ℕ) → is-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) → is-decidable (P s) claim s = dec (p (cons s 0̄)) (p (cons s 1̄)) LM : {X : Set} → (_~_ : X → X → Set) → (∀(x₀ x₁ : X) → is-decidable (x₀ ~ x₁)) → (₂ℕ → X) → ℕ → ℕ LM _~_ dec p 0 = 0 LM _~_ dec p (succ n) = cases 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 {ℕ} _＝_ ℕ-is-discrete LM-₂ : (₂ℕ → 𝟚) → ℕ → ℕ LM-₂ = LM {𝟚} _＝_ 𝟚-is-discrete Lemma[LM]₀ : {X : Set} → (_~_ : X → X → Set) → (dec : ∀(x₀ x₁ : X) → is-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 (cases _ _) 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) → is-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 (cases _ _) r Lemma[succ-0̄-1̄] : {X : Set} → (_~_ : X → X → Set) → (∀(x₀ x₁ : X) → is-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 (inl ∘ sclaim₀) (inr ∘ sclaim₁) (𝟚-possibilities _) 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α = cases 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 (inl ∘ sclaim₀) (inr ∘ sclaim₁) (𝟚-possibilities _) eqβ : p β ~ p (cons s 0̄) eqβ = cases subclaim₃ subclaim₄ subclaim₅ Lemma[LM-modulus] : {X : Set} → (_~_ : X → X → Set) → (dec : ∀(x₀ x₁ : X) → is-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 = cases 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) → is-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 = cases 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₂ : is-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) → is-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] _＝_ ℕ-is-discrete _⁻¹ _∙_ Lemma[LM-₂-least-modulus] : ∀(p : ₂ℕ → 𝟚) → (n : ℕ) → (∀(α β : ₂ℕ) → α ＝⟦ n ⟧ β → p α ＝ p β) → Σ-min \(k : ℕ) → ∀(α β : ₂ℕ) → α ＝⟦ k ⟧ β → p α ＝ p β Lemma[LM-₂-least-modulus] = Lemma[LM-least-modulus] _＝_ 𝟚-is-discrete _⁻¹ _∙_Identity map is uniformly continuous. Function composition preserves uniform continuity. Concatenation maps are uniformly continuous.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 ₁)⁻¹) zero-is-not-one 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))