Effectivizing Lusin’s Theorem #
RUSSELL MILLER
The paper discusses Turing degrees among other things. Here we formalize Turing reducibility (Degrees of unsolvability).
(Mathlib has a reduce.lean
file that can be reconciled with this.)
This file introduces many-one reducibility (mapping reducibility) and proves its basic properties.
We work with a couple of classes of functions:
- mon (which includes both 𝓓₁ and 𝓓ₘ and any monoid of functions)
- mon₁ (which fits 𝓓₁ and 𝓓ₘ but not as general as mon₁)
- monₘ (which includes 𝓓ₘ but not 𝓓₁).
We show over mon₁ that the degrees are not rigid, using complementation.
Over monₘ we show that the degrees form an upper semilattice and has an automorphism that simply swaps ⊥ := ⟦∅⟧ₘ and ⊤ := ⟦ℕ⟧ₘ.
The halting problem K
is defined in this context and
its basic degree-theoretic properties established.
The injective functions ca be used in defining 1-degrees, 𝓓₁.
Equations
- injClone = { func := Function.Injective, id := ⋯, comp := ⋯, inl := injClone.proof_1, inr := injClone.proof_2 }
Instances For
Equations
- instFintypeForallFinBool_marginis u n = Pi.fintype
Equations
- instPrimcodableForallFinBool_marginis n = Primcodable.finArrow
Equations
- instPrimcodableForallFinBool_marginis_1 u n = Primcodable.finArrow
Equations
- instPrimcodableForallFinSuccBool_marginis k = Primcodable.finArrow
Equations
- instDenumerableSigmaNatForallFinBool_marginis u = Denumerable.ofEncodableOfInfinite ((n : ℕ) × (Fin (u n) → Bool))
Equations
- instPrimcodableForallFinOfNatNatBool_marginis = Primcodable.finArrow
Equations
- instEncodableForallBool_marginis = Encodable.fintypeArrowOfEncodable
Equations
- instEncodableListBool_marginis = List.encodable
Equations
- instEncodableListFinOfNatNat_marginis = List.encodable
- self: ∀ {A : ℕ →. ℕ}, Partrec_in A
- zero: ∀ {A : ℕ →. ℕ}, Partrec_in (pure 0)
- succ: ∀ {A : ℕ →. ℕ}, Partrec_in ↑Nat.succ
- left: ∀ {A : ℕ →. ℕ}, Partrec_in fun (n : ℕ) => ↑(some (Nat.unpair n).1)
- right: ∀ {A : ℕ →. ℕ}, Partrec_in fun (n : ℕ) => ↑(some (Nat.unpair n).2)
- pair: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in fun (n : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => g n
- comp: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in fun (n : ℕ) => g n >>= f
- prec: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in (Nat.unpaired fun (a n : ℕ) => Nat.rec (f a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH g (Nat.pair a (Nat.pair y i))) n)
- rfind: ∀ {A f : ℕ →. ℕ}, Partrec_in f → Partrec_in fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)
Instances For
Equations
- Computable_in f g = Partrec_in ↑f
Instances For
Equations
- T_reducible A B = Computable_in (fun (k : ℕ) => (A k).toNat) fun (k : ℕ) => (B k).toNat
Instances For
Equations
- «term_≤ₜ_» = Lean.ParserDescr.trailingNode `term_≤ₜ_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₜ ") (Lean.ParserDescr.cat `term 51))
Instances For
- compu: ∀ {A : ℕ → ℕ} {g : ℕ →. ℕ} {k : ℕ}, Nat.Partrec g → use_bound g k 0
- self: ∀ {A : ℕ → ℕ} {k : ℕ}, use_bound (↑A) k k.succ
- pair: ∀ {A : ℕ → ℕ} {f g : ℕ →. ℕ} {k uf ug : ℕ}, use_bound f k uf → use_bound g k ug → use_bound (fun (n : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => g n) k (max uf ug)
- comp: ∀ {A : ℕ → ℕ} {f g : ℕ →. ℕ} {k uf ug : ℕ} (h : g k ≠ Part.none), use_bound f ((g k).get ⋯) uf → use_bound g k ug → use_bound (fun (n : ℕ) => g n >>= f) k (max uf ug)
Instances For
Equations
- T_equivalent A B = (T_reducible A B ∧ T_reducible B A)
Instances For
Equations
- 𝓓_setoid = { r := T_equivalent, iseqv := t_equiv_equiv }
The Turing degree 0 contains all computable sets, but by definition it is just the Turing degree of ∅.
Equations
- instZero𝓓ₜ = { zero := ⟦fun (x : ℕ) => false⟧ }
Equations
- turing_reducible' A B = Partrec_in A
Instances For
A ≤ₘ B iff A is many-one reducible to B.
Equations
- «term_≤ₘ_» = Lean.ParserDescr.trailingNode `term_≤ₘ_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₘ ") (Lean.ParserDescr.cat `term 51))
Instances For
A ≡ₘ B iff A is many-one equivalent to B.
Equations
- «term_≡ₘ_» = Lean.ParserDescr.trailingNode `term_≡ₘ_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ₘ ") (Lean.ParserDescr.cat `term 51))
Instances For
To do calc proofs with m-reducibility we create a Trans instance.
Equations
- instTransForallNatBoolM_reducible = { trans := ⋯ }
Equivalent reals have equal upper cones.
For example 𝓓₁ is a partial order (if not a semilattice).
Equations
- instPartialOrder𝓓 = PartialOrder.mk ⋯
Make sure ♯ binds stronger than ≤ₘ.
Equations
- «term_⊕__1» = Lean.ParserDescr.trailingNode `term_⊕__1 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 71))
Instances For
Swapping ∅ and ℕ is surjective on 𝓓ₘ.
An automorphism of a partial order is a bijection that preserves and reflects the order.
Equations
- automorphism π = (Function.Bijective π ∧ ∀ (a b : α), a ≤ b ↔ π a ≤ π b)
Instances For
The complement map on 𝓓ₘ.
Equations
- complementMap = Quotient.lift (fun (A : ℕ → Bool) => ⟦cpl A⟧) ⋯
Instances For
A partial order is rigid if there are no nontrivial automorphisms.
Equations
- rigid α = ∀ (π : α → α), automorphism π → π = id
Instances For
An arithmetical characterization of "Even" is primitive recursive.
The usual join of functions on ℕ is computable.
Requirement for a semilattice like 𝓓ₘ.
Instances For
- id : self.func id
- inl : self.func inlFun
- inr : self.func inrFun
- ttrefl : self.func fun (n : ℕ) => Encodable.encode ((Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).snd ↑(Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).fst)
Instances For
The computable functions satisfy the requirement for a semilattice like 𝓓ₘ.
Equations
- comput = { func := Computable, id := comput.proof_1, comp := @comput.proof_2, inl := comput.proof_3, inr := comput.proof_4, join := ⋯, const := comput.proof_5 }
Instances For
The primitive recursive functions satisfy the requirement for a semilattice like 𝓓ₘ.
Equations
- primrec = { func := Primrec, id := primrec.proof_1, comp := @primrec.proof_2, inl := Primrec.nat_double, inr := Primrec.nat_double_succ, join := ⋯, const := primrec.proof_3 }
Instances For
𝓓ₘ is a join-semilattice.
Equations
- instSemilatticeSup𝓓 = SemilatticeSup.mk ⋯ ⋯ ⋯
The complement map is not the identity map of 𝓓ₘ.
The complement map is a surjective map of 𝓓ₘ.
The complement map is an injective map of 𝓓ₘ.
The complement map is an automorphism of 𝓓ₘ.
Over a rich enough monoid, botSwap
is an automorphism.
Defining the halting set K as {e | φₑ(0)↓}. (There are other possible, essentially equivalent, definitions.)
Equations
- K e = decide ((Denumerable.ofNat Nat.Partrec.Code e).eval 0).Dom
Instances For
The complement of the halting set K is not computable.
If B is computable and A ≤ₘ B then A is computable.