Proved several lemmas

ode/AbstractIntegration.v

@@ -834,25 +834,56 @@ Proof. now rewrite rings.flip_negate, rings.negate_involutive. Qed.
 
 End RingFacts.
 
+Import interfaces.orders.
+
+Lemma join_comm `{JoinSemiLatticeOrder L} : Commutative join.
+Proof.
+intros x y. apply antisymmetry with (R := (≤)); [apply _ | |];
+(apply join_lub; [apply join_ub_r | apply join_ub_l]).
+(* why is [apply _] needed? *)
+Qed.
+
+Lemma meet_comm `{MeetSemiLatticeOrder L} : Commutative meet.
+Proof.
+intros x y. apply antisymmetry with (R := (≤)); [apply _ | |];
+(apply meet_glb; [apply meet_lb_r | apply meet_lb_l]).
+Qed.
+
 Definition Range (T : Type) := prod T T.
 
 Instance contains_Q : Contains Q (Range Q) := λ x s, (fst s ⊓ snd s ≤ x ≤ fst s ⊔ snd s).
 
 Lemma Qrange_comm (a b x : Q) : x ∈ (a, b) <-> x ∈ (b, a).
-Admitted.
+Proof.
+unfold contains, contains_Q; simpl.
+rewrite join_comm, meet_comm; reflexivity.
+Qed.
 
 Lemma range_le (a b : Q) : a ≤ b -> forall x, a ≤ x ≤ b <-> x ∈ (a, b).
-Admitted.
+Proof.
+intros A x; unfold contains, contains_Q; simpl.
+mc_setoid_replace (meet a b) with a by now apply lattices.meet_l.
+mc_setoid_replace (join a b) with b by now apply lattices.join_r. reflexivity.
+Qed.
 
 Lemma CRabs_negate (x : CR) : abs (-x) = abs x.
 Proof.
 change (abs (-x)) with (CRabs (-x)).
 rewrite CRabs_opp; reflexivity.
 Qed.
 
+Lemma mspc_ball_Qle (r a x : Q) : mspc_ball r a x <-> a - r ≤ x ≤ a + r.
+Proof. rewrite mspc_ball_Qabs; apply Qabs_diff_Qle. Qed.
+
 Lemma mspc_ball_convex (x1 x2 r a x : Q) :
   mspc_ball r a x1 -> mspc_ball r a x2 -> x ∈ (x1, x2) -> mspc_ball r a x.
-Admitted.
+Proof.
+intros A1 A2 A3.
+rewrite mspc_ball_Qle in A1, A2. apply mspc_ball_Qle.
+destruct A1 as [A1' A1'']; destruct A2 as [A2' A2'']; destruct A3 as [A3' A3'']. split.
++ now transitivity (meet x1 x2); [apply meet_glb |].
++ now transitivity (join x1 x2); [| apply join_lub].
+Qed.
 
 Section IntegralTotal.
 

ode/Picard.v

@@ -241,11 +241,16 @@ assert (B : ball rx x0 x0) by (apply mspc_refl; solve_propholds).
 apply (lip_nonneg (λ y, v ((x0 ↾ B), y)) L).
 Qed.
 
+(* Needed to apply Banach fixpoint theorem, which requires a finite
+distance between any two points *)
 Instance uc_msd : MetricSpaceDistance (UniformlyContinuous sx sy) := λ f1 f2, 2 * ry.
 
 Instance uc_msc : MetricSpaceClass (UniformlyContinuous sx sy).
 Proof.
-intros f1 f2. admit.
+intros f1 f2. unfold msd, uc_msd. intro x. apply (mspc_triangle' ry ry y0).
++ change (to_Q ry + to_Q ry = 2 * (to_Q ry)). ring.
++ apply mspc_symm; apply (proj2_sig (func f1 x)).
++ apply (proj2_sig (func f2 x)).
 Qed.
 
 (*Check _ : MetricSpaceClass sx.
@@ -278,13 +283,9 @@ Definition picard'' (f : UniformlyContinuous sx sy) : UniformlyContinuous sx CR.
 apply (Build_UniformlyContinuous (restrict (picard' f) x0 rx) _ _).
 Defined.
 
+(* Needed below to be able to apply (order_preserving (.* M)) *)
 Instance M_nonneg : PropHolds (0 ≤ M).
-Proof.
-Admitted.
-(*assert (Ax : mspc_ball rx x0 x0) by apply mspc_refl, (proj2_sig rx).
-assert (Ay : mspc_ball ry y0 y0) by apply mspc_refl, (proj2_sig ry).
-apply CRle_Qle. transitivity (abs (v (x0 ↾ Ax , y0 ↾ Ay))); [apply CRabs_nonneg | apply v_bounded].
-Qed.*)
+Proof. apply (bounded_nonneg v). Qed.
 
 Lemma picard_sy (f : UniformlyContinuous sx sy) (x : sx) : ball ry y0 (picard'' f x).
 Proof.

ode/metric.v

@@ -293,7 +293,14 @@ Global Instance Linf_product_msd : MetricSpaceDistance (X * Y) :=
   λ a b, join (msd (fst a) (fst b)) (msd (snd a) (snd b)).
 
 Global Instance Linf_product_mspc_distance : MetricSpaceClass (X * Y).
-Admitted.
+Proof.
+intros z1 z2; split.
+(* Without unfolding Linf_product_msd, the following [apply join_ub_l] fails *)
++ apply (mspc_monotone (msd (fst z1) (fst z2)));
+  [unfold msd, Linf_product_msd; apply join_ub_l | apply mspc_distance].
++ apply (mspc_monotone (msd (snd z1) (snd z2)));
+  [unfold msd, Linf_product_msd; apply join_ub_r | apply mspc_distance].
+Qed.
 
 End ProductMetricSpace.
 
@@ -710,12 +717,11 @@ Global Instance together_uc
   `{ExtMetricSpaceClass X1, ExtMetricSpaceClass Y1, ExtMetricSpaceClass X2, ExtMetricSpaceClass Y2}
    (f1 : X1 -> Y1) (f2 : X2 -> Y2)
   `{!IsUniformlyContinuous f1 mu1, !IsUniformlyContinuous f2 mu2} :
-  IsUniformlyContinuous (together f1 f2) (λ e, meet (mu1 e) (mu2 e)).
+  IsUniformlyContinuous (together f1 f2) (λ e, min (mu1 e) (mu2 e)).
 Proof.
-Admitted.
-(*
 constructor.
-+ intros e e_pos. apply min_ind; [apply (uc_pos f1) | apply (uc_pos f2)]; trivial. (* or use lt_min *)
++ intros e e_pos. (* [apply min_ind] does not work if the goal has [meet] instead of [min] *)
+  apply lt_min; [apply (uc_pos f1) | apply (uc_pos f2)]; trivial.
   (* [trivial] solves, in particular, [IsUniformlyContinuous f1 mu1], which should
      have been solved automatically *)
 + intros e z z' e_pos [A1 A2]. split; simpl.
@@ -724,22 +730,9 @@ constructor.
   - apply (uc_prf f2 mu2); trivial.
     apply (mspc_monotone' (min (mu1 e) (mu2 e))); [apply: meet_lb_r | trivial].
 Qed.
-*)
 
 End ProductSpaceFunctions.
 
-(*
-Section Test.
-
-Context `{ExtMetricSpaceClass A, ExtMetricSpaceClass B, ExtMetricSpaceClass C}
-  (f : A -> B) `{!IsUniformlyContinuous f f_mu}
-  (v : A * B -> C) `{!IsUniformlyContinuous v v_mu}.
-
-Check _ : IsUniformlyContinuous (v ∘ (together id f) ∘ diag) _.
-
-End Test.
-*)
-
 Section CompleteMetricSpace.
 
 Context `{MetricSpaceBall X}.