Library HoTT.Misc.FanTheorem
Require Import Basics Types.
Require Import Truncations.Core.
Require Import Spaces.Nat.Core.
Require Import Misc.UStructures BarInduction.
Require Import Spaces.NatSeq.Core Spaces.NatSeq.UStructure.
Require Import Spaces.List.Core Spaces.List.Theory.
Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Open Scope list_scope.
Definition DecidableFanTheorem (A : Type) :=
∀ (B : list A → Type)
(dec : ∀ l : list A, Decidable (B l))
(bar : IsBar B),
IsUniformBar B.
Definition MonotoneFanTheorem (A : Type) :=
∀ (B : list A → Type)
(mon : IsMonotone B)
(bar : IsBar B),
IsUniformBar B.
Definition FanTheorem (A : Type) :=
∀ (B : list A → Type)
(bar : IsBar B),
IsUniformBar B.
Definition fantheorem_empty : FanTheorem Empty.
Proof.
intros B bB.
∃ 0.
intro s.
contradiction (s 0).
Defined.
Definition fantheorem_contr (A : Type) `{Contr A} : FanTheorem A.
Proof.
intros B bB.
pose (c := fun (_ : nat) ⇒ center A).
∃ (bB c).1.
intro s.
assert (p : ∀ n : nat, list_restrict s n = list_restrict c n).
{ intro n.
srapply path_list_nth'.
1: by rewrite !length_list_restrict.
intros m h.
by apply path_contr. }
∃ (bB c).1; split.
- reflexivity.
- rewrite p.
exact (bB c).2.
Defined.
The family we use when applying the fan theorem in our proof that continuity implies uniform continuity.
Definition uc_theorem_family {A : Type} (p : (nat → A) → Bool)
: list A → Type
:= fun l ⇒
∀ (u v : nat → A) (h : list_restrict u (length l) = l)
(h' : list_restrict v (length l) = l), p u = p v.
Definition is_bar_uc_theorem_family {A : Type}
(p : (nat → A) → Bool) (cont : IsContinuous p)
: IsBar (uc_theorem_family p).
Proof.
intro s.
specialize (cont s 0) as [n H].
∃ n.
intros u v h t.
symmetry in h,t.
rewrite length_list_restrict in h, t.
apply list_restrict_eq_iff_seq_agree_lt in h, t.
exact ((H _ h)^ @ (H _ t)).
Defined.
: list A → Type
:= fun l ⇒
∀ (u v : nat → A) (h : list_restrict u (length l) = l)
(h' : list_restrict v (length l) = l), p u = p v.
Definition is_bar_uc_theorem_family {A : Type}
(p : (nat → A) → Bool) (cont : IsContinuous p)
: IsBar (uc_theorem_family p).
Proof.
intro s.
specialize (cont s 0) as [n H].
∃ n.
intros u v h t.
symmetry in h,t.
rewrite length_list_restrict in h, t.
apply list_restrict_eq_iff_seq_agree_lt in h, t.
exact ((H _ h)^ @ (H _ t)).
Defined.
The fan theorem implies that every continuous function is uniformly continuous. The current proof uses the full fan theorem. Less powerful versions might be enough.
Definition uniform_continuity_fantheorem {A : Type} (fan : FanTheorem A)
(p : (nat → A) → Bool) (c : IsContinuous p)
: uniformly_continuous p.
Proof.
pose proof (fan' := fan (uc_theorem_family p) (is_bar_uc_theorem_family p c)).
destruct fan' as [n ub].
intro m.
∃ n.
intros u v h.
specialize (ub v) as [k [bound uctf]].
apply uctf.
- rewrite length_list_restrict.
apply (snd list_restrict_eq_iff_seq_agree_lt).
apply (us_rel_leq bound h).
- exact (ap _ (length_list_restrict _ _)).
Defined.