Lemmas for Integration
Here we include several lemmas valid in any ordered field F which are useful for integration.
Merging orders
We first prove that any two strictly ordered sets of points which have an empty intersection can be ordered as one (this will be the core of the proof that any two partitions with no common point have a common refinement).
Variable F : COrdField.
Lemma om_fun_lt : forall m n : N, S m < S n -> m < n.
Definition om_fun n m (f : forall i, i < n -> F) (g : forall i, i < m -> F)
(Hfg : forall i j Hi Hj, f i Hi [#] g j Hj) : forall i, i < m + n -> F.
Defined.
Lemma om_fun_1 : forall n m f g Hfg,
nat_less_n_fun f -> nat_less_n_fun g -> nat_less_n_fun (om_fun n m f g Hfg).
Lemma om_fun_2a : forall n m f g Hfg (x : F), (forall i Hi, f i Hi [<] x) ->
(forall i Hi, g i Hi [<] x) -> forall i Hi, om_fun n m f g Hfg i Hi [<] x.
Lemma om_fun_2 : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
(forall i i' Hi Hi', i < i' -> f i Hi [<] f i' Hi') -> (forall i i' Hi Hi', i < i' -> g i Hi [<] g i' Hi')
-> forall i i' Hi Hi', i < i' -> om_fun n m f g Hfg i Hi [<] om_fun n m f g Hfg i' Hi'.
Lemma om_fun_3a : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
forall i Hi, {j : N | {Hj : j < m + n | f i Hi [=] om_fun n m f g Hfg j Hj}}.
Lemma om_fun_3b : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g ->
forall i Hi, {j : N | {Hj : j < m + n | g i Hi [=] om_fun n m f g Hfg j Hj}}.
Lemma om_fun_4a : forall n m f g Hfg (P : F -> CProp), pred_wd F P ->
(forall i Hi, P (f i Hi)) -> (forall j Hj, P (g j Hj)) -> forall k Hk, P (om_fun n m f g Hfg k Hk).
Lemma om_fun_4b : forall n m f g Hfg (P : F -> Prop), pred_wd' F P ->
(forall i Hi, P (f i Hi)) -> (forall j Hj, P (g j Hj)) -> forall k Hk, P (om_fun n m f g Hfg k Hk).
Lemma om_fun_4c : forall n m f g Hfg (P : F -> CProp), pred_wd F P ->
nat_less_n_fun f -> nat_less_n_fun g ->
{i : N | {Hi : i < n | P (f i Hi)}} or {j : N | {Hj : j < m | P (g j Hj)}} ->
{k : N | {Hk : k < m + n | P (om_fun n m f g Hfg k Hk)}}.
Lemma om_fun_4d : forall n m f g Hfg (P : F -> Prop), pred_wd' F P ->
nat_less_n_fun f -> nat_less_n_fun g ->
{i : N | {Hi : i < n | P (f i Hi)}} or {j : N | {Hj : j < m | P (g j Hj)}} ->
{k : N | {Hk : k < m + n | P (om_fun n m f g Hfg k Hk)}}.
Summations
Also, some technical stuff on sums. The first lemma relates two different kinds of sums; the other two ones are variations, where the structure of the arguments is analyzed in more detail.Lemma Sumx_Sum_Sum
: forall n,
Sumx (fun i (H : i < n) => ∑ (f i) (pred (f (S i))) h) [=]
Sumx (fun i (H : i < f n) => h i).
Lemma str_Sumx_Sum_Sum :
forall n (g : (forall i Hi, N -> F)),
(forall i j Hi, f i <= j -> j < f (S i) -> g i Hi j [=] h j) ->
forall m, m = f n ->
Sumx (fun i (H : i < n) => ∑ (f i) (pred (f (S i))) (g i H)) [=]
Sumx (fun i (H : i < m) => h i).
End Lemmas.
Section More_Lemmas.
Variable F : COrdField.
Lemma str_Sumx_Sum_Sum' :
forall (m : N) (f : forall i, i <= m -> N),
f 0 (le_O_n _) = 0 ->
(forall (i j : N) Hi Hj, i = j -> f i Hi = f j Hj) ->
(forall (i j : N) Hi Hj, i < j -> f i Hi < f j Hj) ->
forall (h : N -> F) (n : N) (g : forall i : N, i < m -> N -> F),
(forall (i j : N) Hi Hi' Hi'',
f i Hi' <= j -> j < f (S i) Hi'' -> g i Hi j [=] h j) ->
(forall H, n = f m H) ->
Sumx
(fun (i : N) (H : i < m) =>
∑ (f i (lt_le_weak _ _ H)) (pred (f (S i) H)) (g i H)) [=]
Sumx (fun (i : N) (_ : i < n) => h i).
End More_Lemmas.