Library Lebesgue.subset_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
From Requisite Require Import stdlib.
From Subsets Require Import Subsets_wDep.
Section FU_seq.
Context {E : Type}.
Variable A : nat → E → Prop.
Definition layers : nat → E → Prop :=
fun n ⇒ match n with
| 0%nat ⇒ A 0%nat
| S n ⇒ fun x ⇒ A (S n) x ∧ ¬ A n x
end.
Lemma layers_incl : ∀ n x, layers n x → A n x.
Proof.
intros n x; case n; now simpl.
Qed.
Lemma layers_union :
(∀ n x, A n x → A (S n) x) →
∀ n x, A n x → ∃ m, (m ≤ n)%nat ∧ layers m x.
Proof.
intros HA n x HASn.
induction n.
now ∃ 0%nat.
case (in_dec (A n) x); intros HAn.
destruct IHn as [m [Hm HB]]; try easy; ∃ m; now split; [ lia | ].
now ∃ (S n).
Qed.
Lemma layers_union_alt :
(∀ n x, A n x → A (S n) x) →
∀ n x, (∃ m, (m ≤ n)%nat ∧ layers m x) → A n x.
Proof.
intros HA n x.
induction n; intros [m [Hm HBn]].
apply layers_incl; replace m with 0%nat in HBn; [ easy | lia ].
case (le_lt_dec m n); intros Hm'.
apply HA, IHn; now ∃ m.
apply layers_incl; replace (S n) with m; [ easy | lia ].
Qed.
Lemma layers_union_countable :
(∀ n x, A n x → A (S n) x) →
∀ x, (∃ n, A n x) →
∃ n, layers n x.
Proof.
intros HA x [na HAn].
assert (HBm : ∃ n m, (m ≤ n)%nat ∧ layers m x).
∃ na; apply layers_union; try easy.
destruct HBm as [nb [mb [Hmb HBm]]]; now ∃ mb.
Qed.
Lemma layers_disjoint :
(∀ n x, A n x → A (S n) x) →
∀ n m x, layers n x → layers m x → n = m.
Proof.
intros HA.
assert (HA' : ∀ n m x, (n < m)%nat → A n x → A m x).
intros n m x Hnm HAn.
induction m; try lia.
apply HA.
destruct (ifflr (Nat.lt_eq_cases n m)) as [nltm | ->]; try easy.
now apply Nat.lt_succ_r.
now apply IHm.
assert (HBA' : ∀ n x, layers (S n) x → A n x → False).
intros n x HBSn HAn; now unfold layers in HBSn.
assert (HBA'' : ∀ n m x,
(n < m)%nat → layers m x → A n x → False).
intros n m x Hnm HAn HBm.
apply HBA' with (pred m) x.
replace (S (pred m)) with m; [ easy | lia ].
case (ifflr (Nat.lt_eq_cases n (pred m))); try lia; intros Hn.
apply HA' with n; try easy.
now replace (pred m) with n.
assert (HB : ∀ n m x,
(n < m)%nat → layers n x → layers m x → False).
intros n m x Hnm HBn HBm.
apply HBA'' with n m x; try easy.
now apply layers_incl.
intros n m x HBn HBm.
case (Nat.lt_total n m); intros Hnm.
exfalso; now apply HB with n m x.
destruct Hnm; try easy.
exfalso; now apply HB with m n x.
Qed.
Definition layers_from_above : nat → nat → E → Prop :=
fun n0 n x ⇒ A n0 x ∧ ¬ A (n0 + n)%nat x.
Lemma layers_from_above_incr :
∀ n0,
(∀ n x, A (S n) x → A n x) →
∀ n x, layers_from_above n0 n x → layers_from_above n0 (S n) x.
Proof.
intros n0 HA.
induction n; intros x [HB HB'].
destruct HB'; replace (n0 + 0)%nat with n0; [easy|ring].
split; try easy.
intros H; destruct HB'; apply HA.
replace (S (n0 + S n)) with (n0 + S (S n))%nat; [easy|ring].
Qed.
Lemma layers_from_above_union :
∀ n0,
(∀ n x, A (S n) x → A n x) →
∀ x,
(∃ n1, layers_from_above n0 n1 x) ↔
(A n0 x ∧ ¬ (∀ n, A (n0 + n)%nat x)).
Proof.
intros n0 HA x; split.
intros [n1 [HA0 HA0']]; split; try easy; intros HA0''; now destruct HA0'.
intros [HA0 HA0']; apply not_all_ex_not in HA0';
destruct HA0' as [n HA0n]; now ∃ n.
Qed.
Lemma subset_decr_shift :
(∀ n x, A (S n) x → A n x) →
∀ n0 n x , A (n0 + n)%nat x → A n0 x.
Proof.
intros HAn n0 n x; induction n; intros H.
replace n0 with (n0 + 0)%nat; [easy|ring].
apply IHn, HAn; replace (S (n0 + n)) with (n0 + S n)%nat; [easy|ring].
Qed.
Definition partial_union : nat → E → Prop :=
fun n x ⇒ ∃ m, (m ≤ n)%nat ∧ A m x.
Lemma partial_union_nondecr :
∀ n x, partial_union n x → partial_union (S n) x.
Proof.
intros n x HAn.
case (in_dec (A (S n)) x); intros HAn'.
now ∃ (S n).
destruct HAn as [m [Hm HAm]]; ∃ m; split; [ lia | easy ].
Qed.
Lemma partial_union_union :
∀ x, (∃ n, A n x) ↔ (∃ n, partial_union n x).
Proof.
intros x; split; intros [n HAn].
∃ n; now ∃ n.
destruct HAn as [m [Hm HAm]]; now ∃ m.
Qed.
End FU_seq.
Section DU_seq.
Context {E : Type}.
Definition DU : (nat → E → Prop) → nat → E → Prop :=
fun A n x ⇒
match n with
| 0%nat ⇒ A 0%nat x
| S n ⇒ A (S n) x ∧ ¬ (∃ p, (p ≤ n)%nat ∧ A p x)
end.
Lemma DU_incl :
∀ (A : nat → E → Prop) n x,
DU A n x → A n x.
Proof.
intros A; induction n; try easy.
now intros x [Hn _].
Qed.
Lemma DU_disjoint_alt :
∀ (A : nat → E → Prop) n p x,
(p < n)%nat → DU A n x → ¬ DU A p x.
Proof.
intros A n p x H Hn Hp.
case_eq n; try lia.
intros n' Hn'.
rewrite Hn' in H, Hn; clear Hn' n.
destruct Hn as [H1 H2].
apply DU_incl in Hp.
contradict H2.
∃ p; split; [lia | easy].
Qed.
Lemma DU_disjoint :
∀ (A : nat → E → Prop) n p x,
DU A n x → DU A p x → n = p.
Proof.
intros A n p x Hn Hp.
case (lt_eq_lt_dec n p); [intros [H | H] | intros H].
contradict Hn; now apply DU_disjoint_alt with (n := p).
easy.
contradict Hp; now apply DU_disjoint_alt with (n := n).
Qed.
Lemma DU_union_alt :
∀ (A : nat → E → Prop) n x,
(∃ p, (p ≤ n)%nat ∧ DU A p x) →
(∃ p, (p ≤ n)%nat ∧ A p x).
Proof.
intros A; induction n; intros x [p [Hp Hpx]];
∃ p; split; try easy; now apply DU_incl.
Qed.
Lemma DU_union :
∀ (A : nat → E → Prop) n x,
(∃ p, (p ≤ n)%nat ∧ A p x) →
(∃ p, (p ≤ n)%nat ∧ DU A p x).
Proof.
assert (H : ∀ (A B : E → Prop) x, A x ∨ B x → A x ∨ B x ∧ ¬ A x).
intros A B x.
case (in_dec A x).
intros H _; now left.
intros H [H' | H'].
contradiction.
right; now split.
intros A n x; induction n; intros [p [Hp Hpx]].
∃ p; split; try easy.
rewrite Nat.le_0_r in Hp; rewrite Hp in Hpx; now rewrite Hp.
destruct H
with (A := fun x ⇒ ∃ p, (p ≤ n)%nat ∧ A p x)
(B := fun x ⇒ A (S n) x) (x := x) as [H' | H'].
case (le_lt_eq_dec p (S n)); try easy; clear Hp; intros Hp.
left; ∃ p; split; [lia | easy].
right; now rewrite Hp in Hpx.
destruct H' as [p' Hp'].
destruct IHn as [i [Hi Hix]].
now ∃ p'.
∃ i; split; [lia | easy].
now ∃ (S n).
Qed.
Lemma DU_union_countable :
∀ (A : nat → E → Prop) x,
(∃ n, DU A n x) ↔ (∃ n, A n x).
Proof.
intros A x; split; intros [n Hn].
destruct (DU_union_alt A n x) as [p Hp].
∃ n; split; [lia | easy].
now ∃ p.
destruct (DU_union A n x) as [p Hp].
∃ n; split; [lia | easy].
now ∃ p.
Qed.
Lemma DU_equiv :
∀ (A : nat → E → Prop) n x,
DU A n x ↔ A n x ∧ (∀ p, (p < n)%nat → ¬ A p x).
Proof.
intros A n x; destruct n; try easy.
split; intros [HSn Hn]; split; try easy.
intros p Hp Hp'; apply (Nat.lt_succ_r) in Hp; apply Hn.
∃ p; split; try easy.
now apply Nat.succ_le_mono, Nat.succ_le_mono.
intros Hp; destruct Hp as [p [plen HA]]; apply (Hn p); try easy.
now apply Nat.succ_le_mono in plen.
Qed.
End DU_seq.