Library FEM.geometry

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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.
This file is about the convex_envelop of a set of points in a vector space. It includes the definition and a few lemmas about it.

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Algebra Require Import Algebra_wDep.

Local Open Scope R_scope.

Section Convex_envelop.

Context {E : ModuleSpace R_Ring}.

Inductive convex_envelop {n} (V : 'E^n) : E Prop :=
  | Cvx : (L : 'R^n), ( i, 0 L i) sum L = 1
      convex_envelop V (lin_comb L V).

Lemma convex_envelop_ex :
   {n} (V : 'E^n) x, convex_envelop V x
     (L : 'R^n), ( i, 0 L i) sum L = 1 x = lin_comb L V.
Proof.
intros n V x; split.
intros [L HL1 HL2]; L; easy.
intros [L [HL1 [HL2 HL3]]]; subst; easy.
Qed.

Lemma convex_envelop_inclF :
   {n} (V : 'E^n), inclF V (convex_envelop V).
Proof.
intros n V i; rewrite -lc_kron_l_in_r; apply Cvx.
intros j; apply kronR_bound.
rewrite sum_kron_r; easy.
Qed.

Lemma convex_envelop_castF :
   {n1 n2} (H : n1 = n2) (V1 : 'E^n1) (V2 : 'E^n2),
    V2 = castF H V1 convex_envelop V1 = convex_envelop V2.
Proof. intros; subst; rewrite castF_id; easy. Qed.

End Convex_envelop.

Section Non_deg.

Context {E : ModuleSpace R_Ring}.

Definition non_deg {n:nat} (v:'E^n.+1) :=
   i, convex_envelop v convex_envelop (skipF v i).

Lemma aff_ind_non_deg : {n:nat} (v:'E^n.+1),
  affine_independent v non_deg v.
Proof.
intros n v H i.
assert (H0: x:E,
  convex_envelop v x ¬ convex_envelop (skipF v i) x).
(v i); split.
apply convex_envelop_inclF.
intros H1; inversion H1 as [L HL].
assert (insertF L 0 i = kronR i).
apply affine_independent_lc with v; try easy.
rewrite sum_insertF H0.
rewrite sum_kron_r// plus_zero_l; easy.
rewrite lc_kron_l_in_r.
rewrite lc_insertF_l.
rewrite scal_zero_l H2 plus_zero_l; easy.
specialize (fun_ext_rev H3 i).
simpl; rewrite kronR_is_1; try easy.
rewrite insertF_correct_l; try easy.
auto with real.
destruct H0 as (x,(Hx1,Hx2)).
intros H1.
apply Hx2.
rewrite -H1; easy.
Qed.

End Non_deg.