Library Lebesgue.LF_subcover

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, 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.
LF means leap-frog: open intervals of a (finite) cover are selected such that the next interval contains the current right bound.
This is useful for the construction of the Lebesgue measure on R.

From Requisite Require Import stdlib_wR.
From Coq Require Import FinFun List Sorted.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Logic Require Import logic_compl.
From Lebesgue Require Import list_compl sort_compl R_compl.

Local Open Scope R_scope.

Section LF_subcover_N.


Variable a b : R.

Hypothesis Sab : a b.

Variable an bn : nat R.

Variable N : nat.

Definition Index : (nat Prop) R Set :=
  fun InJ x{ i | InJ i an i < x < bn i }.

Lemma Index_In :
   (InJ : nat Prop) x (iJx : Index InJ x),
    let i := proj1_sig iJx in
    InJ i.
Proof.
intros InJ x iJx.
apply (proj1 (proj2_sig iJx)).
Qed.

Lemma Index_cover :
   (InJ : nat Prop) x (iJx : Index InJ x),
    let i := proj1_sig iJx in
    an i < x < bn i.
Proof.
intros InJ x iJx.
apply (proj2 (proj2_sig iJx)).
Qed.

Definition Cover_r : (nat Prop) R Set :=
  fun InJ x z, x z b Index InJ z.

Definition In0N : nat Prop := fun j ⇒ (j N)%nat.

Hypothesis C0Nab : Cover_r In0N a.

Lemma next_Index :
   (InJ : nat Prop) x,
    Cover_r InJ x x b Index InJ x.
Proof.
intros InJ x CJxb Sxb.
destruct (CJxb x) as [i [Hi1 [Hi2 Hi3]]].
split; try easy; now apply Rle_refl.
i; now repeat split.
Qed.

Definition is_len : nat (nat Prop) Prop :=
  fun lenJ InJ
     (lJ : list nat),
      ( j, InJ j In j lJ)
      NoDup lJ length lJ = lenJ.

Lemma next_InJ_length :
   lenJ' (InJ : nat Prop) x
      (CJxb : Cover_r InJ x) (Sxb : x b),
    let iJx := next_Index InJ x CJxb Sxb in
    let i' := proj1_sig iJx in
    let InJ' := fun jInJ j j i' in
    is_len (S lenJ') InJ is_len lenJ' InJ'.
Proof.
intros lenJ' InJ x CJxb Sxb iJx i' InJ' [lJ [H1 [H2 H3]]].
destruct lJ as [ | j0 l]; try easy.
case (Nat.eq_dec j0 i'); intros Hj0.
rewrite NoDup_cons_iff in H2; destruct H2 as [H21 H22].
simpl in H3; apply Nat.succ_inj in H3.
(select (fun jj i') l).
rewrite Hj0 in H1, H21; clear Hj0 j0.
rewrite select_True.
2: intros j Hj1 Hj2; now rewrite Hj2 in Hj1.
split; [ | now split].
intros j; unfold InJ'; specialize (H1 j); rewrite H1; repeat split.
intros [Hj1 Hj2]; apply in_inv in Hj1;
    destruct Hj1 as [Hj1 | Hj1]; try easy.
now symmetry in Hj1.
now apply in_cons.
intros Hj; now rewrite Hj in H.
generalize (Index_In InJ x iJx); fold i'; simpl; intros Hi'.
rewrite H1 in Hi'.
(select (fun jj i') (j0 :: l)).
split.
intros j; unfold InJ'; specialize (H1 j); rewrite H1; split.
intros [Hj1 Hj2]; now apply In_select_P_inv.
intros Hj; split.
now apply In_select_In in Hj.
now apply In_select_P in Hj.
split.
now apply NoDup_select.
now apply remove_decr_length.
Qed.

Lemma next_Cover :
   (InJ : nat Prop) x (CJxb : Cover_r InJ x) (Sxb : x b),
    let iJx := next_Index InJ x CJxb Sxb in
    let i' := proj1_sig iJx in
    let InJ' := fun jInJ j j i' in
    let x' := bn i' in
    Cover_r InJ' x'.
Proof.
intros InJ x CJxb Sxb iJx i'.
destruct (proj2_sig iJx) as [Hi1 [Hi2 Hi3]]; fold i' in Hi1, Hi2, Hi3.
intros InJ' x' z [Hz1 Hz2].
destruct (CJxb z) as [j [Hj1 [Hj2 Hj3]]].
split; try easy; now apply Rlt_le, Rlt_le_trans with x'.
j; repeat split; try easy.
intros H.
rewrite H in Hj3.
now apply Rle_not_lt in Hz1.
Qed.

Definition lt_bn : nat nat Prop :=
  fun j1 j2bn j1 < bn j2.

Lemma lt_bn_irrefl : j, ¬ lt_bn j j.
Proof.
intros j Hj.
now apply Rlt_irrefl in Hj.
Qed.

Lemma lt_bn_trans :
   j1 j2 j3, lt_bn j1 j2 lt_bn j2 j3 lt_bn j1 j3.
Proof.
intros j1 j2 j3 H1 H2.
now apply Rlt_trans with (bn j2).
Qed.

Definition P_cover : nat nat Prop :=
  fun j1 j2an j2 < bn j1 lt_bn j1 j2.

Fixpoint LF lenJ (InJ : nat Prop) x
    (CJxb : Cover_r InJ x) (Sxb : x b) : list nat :=
  match lenJ with
  | 0 ⇒ nil
  | S lenJ'
    let i' := proj1_sig (next_Index InJ x CJxb Sxb) in
    let InJ' := fun jInJ j j i' in
    let x' := bn i' in
    let CJ'x'b := next_Cover InJ x CJxb Sxb in
    i' ::
      (match Rlt_le_dec b x' with
      | left _nil
      | right Sx'bLF lenJ' InJ' x' CJ'x'b Sx'b
      end)
  end.

Lemma LF_iter :
   lenJ' (InJ : nat Prop) x
      (CJxb : Cover_r InJ x) (Sxb : x b),
    let i' := proj1_sig (next_Index InJ x CJxb Sxb) in
    let InJ' := fun jInJ j j i' in
    let x' := bn i' in
    let CJ'x'b := next_Cover InJ x CJxb Sxb in
    LF (S lenJ') InJ x CJxb Sxb =
    i' :: (match Rlt_le_dec b x' with
          | left _nil
          | right Sx'bLF lenJ' InJ' x' CJ'x'b Sx'b
          end).
Proof.
intros; now unfold LF.
Qed.


Lemma LF_length :
   lenJ (InJ : nat Prop) x
      (CJxb : Cover_r InJ x) (Sxb : x b),
    (length (LF lenJ InJ x CJxb Sxb) lenJ)%nat.
Proof.
induction lenJ; simpl; try easy; intros InJ x CJxb Sxb.
  pose (i' := proj1_sig (next_Index InJ x CJxb Sxb)); fold i'.
  pose (InJ' := fun jInJ j j i'); fold InJ'.
  pose (x' := bn i'); fold x'.
  pose (CJ'x'b := next_Cover InJ x CJxb Sxb); fold CJ'x'b.
case (Rlt_le_dec _); intros H.
simpl; lia.
  rename H into Sx'b.
apply le_n_S.
apply IHlenJ.
Qed.

Lemma LF_LocallySorted_P_cover :
   lenJ (InJ : nat Prop) x
      (CJxb : Cover_r InJ x) (Sxb : x b),
    LocallySorted P_cover (LF lenJ InJ x CJxb Sxb).
Proof.
induction lenJ; simpl; intros InJ x CJxb Sxb.
apply LSorted_nil.
  pose (i' := proj1_sig (next_Index InJ x CJxb Sxb)); fold i'.
  pose (InJ' := fun jInJ j j i'); fold InJ'.
  pose (x' := bn i'); fold x'.
  pose (CJ'x'b := next_Cover InJ x CJxb Sxb); fold CJ'x'b.
case (Rlt_le_dec _); intros H.
apply LSorted_cons1.
  rename H into Sx'b.
induction lenJ; simpl.
apply LSorted_cons1.
  pose (i'' := proj1_sig (next_Index InJ' x' CJ'x'b Sx'b)); fold i''.
  pose (InJ'' := fun jInJ' j j i''); fold InJ''.
  pose (x'' := bn i''); fold x''.
  pose (CJ''x''b := next_Cover InJ' x' CJ'x'b Sx'b); fold CJ''x''b.
apply LSorted_consn.
2: apply Index_cover.
case (Rlt_le_dec _); intros H.
apply LSorted_cons1.
  rename H into Sx''b.
replace (i'' :: LF lenJ InJ'' x'' CJ''x''b Sx''b)
    with (LF (S lenJ) InJ' x' CJ'x'b Sx'b).
apply IHlenJ.
simpl; fold i'' InJ'' x'' CJ''x''b; f_equal.
case (Rlt_le_dec _); intros H.
apply Rlt_not_le in H; contradiction.
f_equal; apply proof_irrel.
Qed.

Lemma LF_LocallySorted_lt_bn :
   lenJ (InJ : nat Prop) x
      (CJxb : Cover_r InJ x) (Sxb : x b),
    LocallySorted lt_bn (LF lenJ InJ x CJxb Sxb).
Proof.
intros lenJ InJ x CJxb Sxb.
apply LocallySorted_impl1 with (P1 := P_cover).
clear; now intros a b [_ H].
apply LF_LocallySorted_P_cover.
Qed.

Lemma LF_last :
   p lenJ (InJ : nat Prop) x
    (CJxb : Cover_r InJ x) (Sxb : x b),
  is_len lenJ InJ (lenJ p)%nat
  b < bn (last (LF p InJ x CJxb Sxb) 0%nat).
Proof.
induction p.
simpl; intros lenJ InJ x CJxb Sxb HlJ H0.
destruct HlJ as [l [Hl1 [Hl2 Hl3]]].
apply Nat.le_0_r in H0; rewrite H0 in Hl3.
rewrite length_zero_iff_nil in Hl3; rewrite Hl3 in Hl1; simpl in Hl1.
assert (H : x b b) by (split; [apply Sxb | apply Rle_refl]).
generalize (CJxb b H); clear H; intros iJb.
generalize (Index_In InJ b iJb); simpl; intros Hi.
now rewrite Hl1 in Hi.
induction lenJ as [ | lenJ'].
intros InJ x CJxb Sxb HlJ Hp.
destruct HlJ as [l [Hl1 [Hl2 Hl3]]].
rewrite length_zero_iff_nil in Hl3; rewrite Hl3 in Hl1; simpl in Hl1.
assert (H : x b b) by (split; [easy | apply Rle_refl]).
generalize (CJxb b H); clear H; intros iJb.
generalize (Index_In InJ b iJb); simpl; intros Hi.
now rewrite Hl1 in Hi.
intros InJ x CJxb Sxb HlJ Hp.
rewrite LF_iter.
  pose (i' := proj1_sig (next_Index InJ x CJxb Sxb)); fold i'.
  pose (InJ' := fun jInJ j j i'); fold InJ'.
  pose (x' := bn i'); fold x'.
  pose (CJ'x'b := next_Cover InJ x CJxb Sxb); fold CJ'x'b.
case (Rlt_le_dec _ ); try easy; intros Sx'b.
induction p.
apply (next_InJ_length lenJ' InJ x CJxb Sxb) in HlJ; fold i' InJ' in HlJ.
destruct HlJ as [l [Hl1 [Hl2 Hl3]]].
apply le_S_n, Nat.le_0_r in Hp; rewrite Hp in Hl3.
rewrite length_zero_iff_nil in Hl3; rewrite Hl3 in Hl1; simpl in Hl1.
assert (H : x' b b) by (split; [apply Sx'b | apply Rle_refl]).
generalize (CJ'x'b b H); clear H; intros iJ'b; fold i' InJ' in iJ'b.
generalize (Index_In InJ' b iJ'b); simpl; intros Hi'.
now rewrite Hl1 in Hi'.
  pose (i'' := proj1_sig (next_Index InJ' x' CJ'x'b Sx'b)); fold i''.
  pose (InJ'' := fun jInJ' j j i''); fold InJ''.
  pose (x'' := bn i''); fold x''.
  pose (CJ''x''b := next_Cover InJ' x' CJ'x'b Sx'b); fold CJ''x''b.
specialize (IHp lenJ' InJ' x' CJ'x'b Sx'b); apply IHp.
now apply next_InJ_length.
now apply le_S_n.
Qed.

Definition subcover : list nat := LF (S N) In0N a C0Nab Sab.

Definition q := Nat.pred (length subcover).

Definition i : nat nat := fun pnth p subcover 0%nat.

Lemma SN_is_len_In0N : is_len (S N) In0N.
Proof.
(seq 0 (S N)); unfold In0N; split.
intros j; rewrite in_seq; lia.
split; [apply seq_NoDup | apply length_seq].
Qed.

Lemma subcover_length : (q N)%nat.
Proof.
apply le_S_n.
unfold q; rewrite Nat.succ_pred_pos.
apply LF_length.
simpl; apply Nat.lt_0_succ.
Qed.

Lemma subcover_incr :
   p, (p < q)%nat lt_bn (i p) (i (S p)).
Proof.
intros p Hp.
unfold i; apply LocallySorted_nth.
rewrite Nat.sub_1_r; fold q; lia.
apply LF_LocallySorted_lt_bn.
Qed.

Lemma subcover_monotone :
   p p',
    (p q)%nat (p' q)%nat
    (p < p')%nat lt_bn (i p) (i p').
Proof.
intros p p' Hp Hp' H.
induction p'; try easy.
case (lt_eq_lt_dec p' p); [intros [H' | H'] | intros H'].
contradict H'; lia.
rewrite H'.
apply subcover_incr; lia.
apply lt_bn_trans with (i p').
apply IHp'; lia.
apply subcover_incr; lia.
Qed.

Lemma subcover_inj : bInjective (S q) i.
Proof.
intros p p' Hp Hp' Hpp'.
rewrite Nat.lt_succ_r in Hp, Hp'.
case (lt_eq_lt_dec p p'); [intros [H | H] | intros H].
2: exact H.
all: apply subcover_monotone in H; try easy.
all: rewrite Hpp' in H.
all: now apply lt_bn_irrefl in H.
Qed.

Lemma subcover_bound_l : an (i 0%nat) < a.
Proof.
unfold i; simpl.
apply Index_cover.
Qed.

Lemma subcover_bound_r : b < bn (i q).
Proof.
unfold q, i, subcover; rewrite <- last_nth.
apply LF_last with (lenJ := S N); try easy.
apply SN_is_len_In0N.
Qed.

Lemma subcover_LF :
   p, (p < q)%nat an (i (S p)) < bn (i p).
Proof.
intros p Hp.
apply (LocallySorted_nth P_cover).
now rewrite Nat.sub_1_r.
apply LF_LocallySorted_P_cover.
Qed.

Lemma LF_subcover_N :
    (q N)%nat bInjective (S q) i
    an (i 0%nat) < a b < bn (i q)
     p, (p < q)%nat an (i (S p)) < bn (i p).
Proof.
repeat split.
apply subcover_length.
apply subcover_inj.
apply subcover_bound_l.
apply subcover_bound_r.
apply subcover_LF.
Qed.

End LF_subcover_N.

Section LF_finite_subcover.

Variable a b : R.
Variable an bn : nat R.

Hypothesis Hab : a b.
Hypothesis Cover : x, a x b n, an n < x < bn n.

Lemma open_set_interval :
   a b, open_set (fun xa < x < b).
Proof.
clear; intros a b. case (Rlt_dec a b); intros H.
pose (c := (a + b) × / 2).
pose (r := (b - a) × / 2).
assert (Hr : 0 < r).
  apply Rdiv_lt_0_compat.
  now apply Rlt_0_minus.
  apply Rlt_0_2.
pose (posr := mkposreal r Hr).
apply open_set_P6 with (disc c posr). apply disc_P1. unfold disc; simpl; split; intros x Hx.
rewrite Rabs_lt_between' in Hx.
replace (c - r) with a in Hx.
replace (c + r) with b in Hx; try easy.
1,2: unfold c, r; field.
rewrite Rabs_lt_between'.
replace (c - r) with a.
replace (c + r) with b; try easy.
1,2: unfold c, r; field.
apply open_set_P6 with (fun _ : RFalse). apply open_set_P4. split; intros x Hx; try easy; destruct Hx as [Hx1 Hx2].
now generalize (Rlt_trans _ _ _ Hx1 Hx2); intros H'.
Qed.

Lemma finite_subcover :
   N,
     x, a x b n, (n N)%nat an n < x < bn n.
Proof.
pose (f := fun i yan (R2N i) < y < bn (R2N i)).
assert (Hf : i, ( x, f i x) True) by easy.
pose (cover := mkfamily (fun _True) f Hf).
generalize (compact_P3 a b cover); intros [D [H [l Hl]]].
split.
intros x Hx; destruct (Cover x Hx) as [n Hn]; (INR n).
simpl; unfold f; now rewrite R2N_INR.
intros x; simpl; unfold f.
apply open_set_interval.
(max_l (map R2N l)).
intros x Hx; destruct (H x Hx) as [i [Hi1 Hi2]]; (R2N i).
split; try apply Hi1.
apply max_l_correct, in_map with (f := R2N), Hl; easy.
Qed.

Lemma LF_finite_subcover :
   q (i : nat nat),
    bInjective (S q) i
    an (i 0%nat) < a b < bn (i q)
     p, (p < q)%nat an (i (S p)) < bn (i p).
Proof.
destruct finite_subcover as [N HN].
assert (C0Nab : Cover_r b an bn (In0N N) a).
intros x Hx.
destruct (LPO (fun iIn0N N i an i < x < bn i)) as [[i Hi] | Hi].
intros i; apply classic.
now i.
contradict Hi; apply ex_not_not_all.
specialize (HN x Hx) as [n Hn].
n; intuition.
(q a b Hab an bn N C0Nab); (i a b Hab an bn N C0Nab).
now destruct (LF_subcover_N a b Hab an bn N C0Nab)
    as [_ [H1 [H2 [H3 H4]]]].
Qed.

End LF_finite_subcover.