From 40e3345a98ad3d0a7b0cad562264aec8eab4207a Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 15 Dec 2023 18:31:12 -0500 Subject: [PATCH] resetting unused files --- theories/cantor.v | 104 -------------------------------------------- theories/charge.v | 63 --------------------------- theories/topology.v | 8 ---- 3 files changed, 175 deletions(-) diff --git a/theories/cantor.v b/theories/cantor.v index 429ffbed8..308447c4b 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -537,107 +537,3 @@ by exists f; rewrite -cstf; exact: cst_continuous. Qed. End alexandroff_hausdorff. - -Section cantor_subspace. -Context {T : topologicalType} (A : set T). - -Definition cantor_like_subspace := - [/\ perfect_set A, - compact A, - hausdorff_space T & - totally_disconnected A]. - -Context a0 (Aa0 : A a0). - -Let A' := PointedType (classicType_choiceType {x & A x}) (exist _ _ Aa0). -Let WA := @weak_topologicalType A' T (@projT1 _ A). -Lemma perfect_set_weak : - perfect_set A -> perfect_set [set: WA]. -Proof. -move=> pftA; apply/perfectTP; case=> t At /=. -rewrite /open/=/wopen/=; apply/forallPNP => E oE. -case: (pselect (E t)); first last. - apply: contra_not; rewrite eqEsubset; case=> _ /(_ (existT _ _ At)). - exact. -case: pftA => clA lpA Et; have : A t by done. -rewrite -[a in a _]lpA => /(_ E) []; first exact: open_nbhs_nbhs. -move=> e [+] Ae Ee; apply: contra_neq_not. -rewrite eqEsubset; case=> /(_ (existT _ _ Ae) Ee) /= + _. -exact: EqdepFacts.eq_sigT_fst. -Qed. - -Lemma compact_set_weak : - compact A -> compact [set: WA]. -Proof. -move=> /compact_near_coveringP cptA; apply/ compact_near_coveringP. -move=> ? F /= P FF cvr; pose Q i x := if pselect (A x) is left Ax - then P i (existT _ _ Ax) else True. -have := (@cptA _ F Q FF); have FQ : forall x, A x -> \near x & F, Q F x. - move=> x Ax; have := cvr (existT _ _ Ax) I. - case; case=> E j [/= [? [[V oV /= <- /= Vx VE FJ EJ]]]]. - exists (V, j); first by split => //; apply: open_nbhs_nbhs; split. - case=> /= z i [Vz ji]; rewrite /Q; case: (pselect _) => // Az. - by have := (EJ (existT _ _ Az, i)); apply; split => //; apply: VE. -move/(_ FQ); apply: filter_app; near=> z => + [r /= Ar _] => /(_ _ Ar). -by rewrite /Q; case (pselect _) => // Ar'; suff -> // : Ar = Ar'. -Unshelve. all: end_near. Qed. - -Lemma totally_disconnected_weak : - totally_disconnected A -> totally_disconnected [set: WA]. -Proof. -move=> tdA [x Ax] _; rewrite eqEsubset; split; first last. - by move=> ? ->; exact: connected_component_refl. -move=> [y Ay] [U [Ux _ ctU Uy]] => /=. -apply/eq_existT_curried; last by move=> ?. -have := tdA _ Ax; rewrite eqEsubset; case=> + _; apply. -exists (@projT1 T _ @` U); last by exists (existT _ _ Ay). -split; first by exists (existT _ _ Ax). - by move=> ? [[? ? ? <-]]. -apply: connected_continuous_connected => //. -by apply: continuous_subspaceT; exact: weak_continuous. -Qed. - -Lemma hausdorff_weak : - hausdorff_space T -> hausdorff_space WA. -Proof. -move=> hsdfK [p Ap] [q Aq] /= clstr. -apply/eq_existT_curried; last by move=> ?. -apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]]. -exists (@projT1 T _ @ G); [exact: fmap_proper_filter|split]. - apply: cvg_trans; first (apply:cvg_app; exact: GtoQ). - exact: weak_continuous. -move/(cvg_app (@projT1 T _)): psubG => /cvg_trans; apply. -exact: weak_continuous. -Qed. - -Definition foo {R : realType} (P : set R) (P01 : P `<=` `[0%R,1%R]) : R -> R := - 0%R. - tvf@`P (wlog (tvf 1 = 1)) - - C --> [0,1] --> [0,1] - A A A - | | | - V | | - C <--> P ------> tvf @`P - - -mu (tvf @` P) = eps -mu (f @` P) = mu (((tvf + f)/2 - (tvf - f) /2) ) - -mu (f@` `[a,b]) = - - -Lemma cantor_like_subspaceP : - cantor_like_subspace -> cantor_like WA. -Proof. -case=> /perfect_set_weak ? /compact_set_weak ?. - -Search (existT _ _ _ = existT _ _ _). -pose f x := if pselect (A x) is left Ax then existT _ _ Ax else existT _ _ Aa0. -have -> : [set existT _ _ Ax] = f @` [set x]. - rewrite eqEsubset /f; split => z. - by move=> ->; exists x => //; case (pselect _) => // Ax';suff -> : Ax = Ax'. - by case => ? /= ->; case (pselect _) => // Ax'; suff -> : Ax = Ax'. - -apply: connected_component_max. -End cantor_subspace. diff --git a/theories/charge.v b/theories/charge.v index c66fce0a3..b56ebf1f3 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -583,69 +583,6 @@ Qed. End positive_negative_set_realFieldType. -Section absolute_continuity. -Context {R : realType}. -Notation mu := (@lebesgue_measure R). - -Lemma interval_measure0 A : is_interval A -> mu A = 0 -> is_subset1 A. -Proof. -Admitted. - -Lemma measure0_disconnected A : - measurable A -> mu A = 0 -> totally_disconnected A. -Proof. -move=> mA A0 x Ax; rewrite eqEsubset; split; first last. - by move=> ? ->; exact: connected_component_refl. -move=> y [U /= [Ux UA /connected_intervalP ]] itvU. -have : mu U = 0. - apply/eqP; rewrite -measure_le0 //= -A0. - by apply: (le_measure); rewrite ?inE //; first exact: is_interval_measurable. -by move/(interval_measure0 itvU) => /[apply]; apply. -Qed. - - - - -Definition maps_null E (f : R -> R) := - forall A, A `<=` E -> mu A = 0%:E -> mu (f @` A) = 0%:E. - -Definition absolutely_continuous a b (f : R -> R) := - [/\ {within `[a,b], continuous f }, - bounded_variation a b f & - maps_null `[a,b] f - ]. - -Lemma maps_null_total_variation (a b : R) f : - (a <= b)%R -> - absolutely_continuous a b f -> - maps_null `[a, b] (fine \o neg_tv a f). -Proof. -move=> ab [ctsf bdf] f0 A AE A0. - -\int[pushforward mu mphi]_(y in (phi @` U)) f y - = \int[mu]_(x in phi^-1 (phi @` U)) (f \o phi) x. - -0 = \int_(f@`A) id - -integralD - -Search measure (0%:E). - -Local Notation TV := (@total_variation R). - -Lemma absolute_continuity_cumulative a b (f : R -> R) : - absolutely_continuous a b f -> exists g h, - [/\ absolutely_continuous a b g, - absolutely_continuous a b h, - {in `[a,b] &, {homo g : x y / x <= y}}, - {in `[a,b] &, {homo h : x y / x <= y}} & - f = g \- h - ]. -Proof. -case => ctsf bdf f0. - -End absolute_continuity. - Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). diff --git a/theories/topology.v b/theories/topology.v index 232d91131..b762064ab 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4063,14 +4063,6 @@ suff : R `&` U = R by move: Rx => /[swap] <- []. by apply: ctdR; [exists z|exists U|exists U]. Qed. -Lemma totally_disconnected_compact {T : topologicalType} : - hausdorff_space T -> - compact [set: T] -> - totally_disconnected [set: T] -> - zero_dimensional T. -Proof. -move=> hsdfT cmpT dctT x y xny. - Lemma totally_disconnected_cvg {T : topologicalType} (x : T) : hausdorff_space T -> zero_dimensional T -> compact [set: T] -> filter_from [set D : set T | D x /\ clopen D] id --> x.