resetting unused files

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.

theories/charge.v

@@ -478,69 +478,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).

theories/topology.v

@@ -3995,14 +3995,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.