Add generalized results ae_modus_ponens_gen and ae_imply_gen.

New version of ae_op_compat is now proved using the previous result.

Lebesgue/measure.v

@@ -894,6 +894,40 @@ apply negligible_ext with (A1 := fun _ => False); try intuition.
 apply negligible_emptyset.
 Qed.
 
+(* Lemma 884 p. 183 (v3) *)
+Lemma ae_modus_ponens_gen :
+  forall (P Q : nat -> (nat -> F) -> Prop),
+    (forall f, ae (fun x => (forall j, P j (fun i => f i x)) ->
+                            (forall k, Q k (fun i => f i x)))) ->
+    forall f, (forall j, ae (fun x => P j (fun i => f i x))) ->
+              (forall k, ae (fun x => Q k (fun i => f i x))).
+Proof.
+intros P Q H f HP k.
+pose (PP := fun f => forall j, P j f).
+pose (QQ := fun f => forall k, Q k f).
+pose (Ax := fun (XX : (nat -> F) -> Prop) f (x : E) => XX (fun i => f i x)).
+pose (B := fun x => (Ax PP f x -> Ax QQ f x) /\ Ax PP f x).
+apply negligible_le with  (fun x => ~ (Ax PP f x -> Ax QQ f x) \/ ~ Ax PP f x).
+intros x HQ; apply not_and_or; intuition.
+apply negligible_union; unfold Ax, PP, QQ.
+unfold ae in H; try easy.
+apply negligible_ext with (fun x => exists j, ~ P j (fun i => f i x)).
+intros; split; [apply ex_not_not_all | apply not_all_ex_not].
+apply negligible_union_countable; easy.
+Qed.
+
+(* Lemma 885 p. 183 (v3) *)
+Lemma ae_imply_gen :
+  forall (P Q : nat -> (nat -> F) -> Prop),
+    (forall (f : nat -> E -> F) x,
+      (forall j, P j (fun i => f i x)) -> (forall k, Q k (fun i => f i x))) ->
+    forall f, (forall j, ae (fun x => P j (fun i => f i x))) ->
+              (forall k, ae (fun x => Q k (fun i => f i x))).
+Proof.
+intros P Q H; apply ae_modus_ponens_gen; intros f.
+apply ae_everywhere; auto.
+Qed.
+
 (* Lemma 646 p. 124 *)
 Lemma ae_modus_ponens :
   forall (A1 A2 : E -> Prop), ae (fun x => A1 x -> A2 x) -> ae A1 -> ae A2.
@@ -1045,6 +1079,36 @@ Context {F : Type}.
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
 
+Lemma ae_op_compat_new :
+  forall (R1 R2 : F -> F -> Prop) (op : (nat -> F) -> F),
+    (forall (f g : nat -> E -> F) x,
+      (forall n, R1 (f n x) (g n x)) ->
+      R2 (op (fun i => f i x)) (op (fun i => g i x))) ->
+    (forall (f g : nat -> E -> F),
+      (forall n, ae mu (fun x => R1 (f n x) (g n x))) ->
+      ae mu (fun x => R2 (op (fun i => f i x)) (op (fun i => g i x)))).
+Proof.
+intros R1 R2 op H f g H1.
+pose (Q := fun k fg => match k with
+  | 0%nat => R2 (op (fun i => fst (fg i))) (op (fun i => snd (fg i)))
+  | S _ => True
+  end).
+apply ae_ext with (fun x => Q 0%nat (fun i => (f i x, g i x))); try easy.
+assert (HQ : forall k, ae mu (fun x => Q k (fun i => (f i x, g i x)))); try easy.
+pose (P := fun j fg => match j with
+  | 0%nat => forall i : nat, R1 (fst (fg i)) (snd (fg i))
+  | S _ => True
+  end).
+apply ae_imply_gen with P.
+(* *)
+intros fg x HP k; destruct k; try easy; simpl.
+apply H with (f := fun i x => fst (fg i x)) (g := fun i x => snd (fg i x)).
+apply (HP 0%nat).
+(* *)
+intros j; destruct j; simpl; try apply ae_True.
+apply ae_inter_countable; easy.
+Qed.
+
 (* Lemma 659 pp. 126-127 (with I = nat) *)
 Lemma ae_op_compat :
   forall (P Q : F -> F -> Prop) (op : (nat -> F) -> F) (y0 : F),