bounded_operator.coq

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix interval.
From mathcomp Require Import boolp reals classical_sets signed topology functions.
From mathcomp Require Import prodnormedzmodule normedtype landau forms derive.
From mathcomp Require Import ring.

Set Implicit Arguments.

Import Order.Theory.
Import GRing.Theory.
Import Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.


Lemma image_nonempty U V (f: U -> V) (A: set U) :
  A !=set0 -> f @` A !=set0.
Proof. by move=> [a Ha]; exists (f a); apply/imageP. Qed.

Lemma image_cst U V (c: V) (A: set U) :
  A !=set0 -> cst c @` A = [set c].
Proof.
move=> NE. apply/seteqP. split=> [+ [] | _ /= ->]=> //.
case: NE=> [x Hx]. by exists x.
Qed.

Section SupTheory.
Context {R: realType}.

(* MAYBE introduce is_inf ? *)
Section SupImage.
Context (f: R -> R).
Hypothesis (Hf: {homo f : x y / x <= y}).

Lemma image_sup_ub (A: set R) : has_ubound A -> ubound (f @` A) (f (sup A)).
Proof. move=> Ub _ [x Hx <-]. by apply/Hf/sup_ub. Qed.

Lemma image_sup_le_sup (A: set R) : has_sup A -> sup (f @` A) <= f (sup A).
Proof.
move=> [NE Ub]. by apply/sup_le_ub; [apply/image_nonempty | apply/image_sup_ub].
Qed.

Lemma image_has_sup (A: set R) : has_sup A -> has_sup (f @` A).
Proof.
move=> [NE Ub]. split; first by apply/image_nonempty.
eexists. by apply/image_sup_ub.
Qed.

End SupImage.

Lemma ex_image_sup_eq (f: R -> R) (A: set R) :
  {mono f : x y / x <= y} -> has_sup A -> (range f) (sup (f @` A)) -> sup (f @` A) = f (sup A).
Proof.
move=> Hf. have HfLe : {homo f : x y / x <= y} by move=> x y; rewrite Hf.
move=> HA [t _ Eqt]. have HfA := image_has_sup HfLe HA.
apply/eqP; rewrite eq_le ?image_sup_le_sup //=.
rewrite -Eqt Hf // sup_le_ub //; first by case: HA.
move=> x Hx. rewrite -Hf Eqt sup_ub //; by case: HfA.
Qed.

(*
  Should generalize to continuous increasing function,
  but would be chore to prove.

  Maybe many parts could be simplified.
*)
Lemma mul_sup_eq (c: R) (A: set R) :
  c >= 0 -> has_sup A -> sup [set c * x | x in A] = c * sup A.
Proof.
rewrite le_eqVlt=> /orP [/eqP <- | Cmp] HA.
- have -> : (fun x : R => 0 * x) = cst 0.
  + apply/funext=> x. by rewrite mul0r.
  rewrite image_cst; first by rewrite sup1 mul0r.
  by case: HA.
- apply/ex_image_sup_eq=> //; first by apply/ler_pmul2l.
  set M := sup [set c * x | x in A]=> /=.
  exists (M / c)=> //. field. by rewrite neq_lt Cmp orbT.
Qed.

End SupTheory.

Section LinearZmod.
Context (R: ringType) (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).

Definition linear_zero : {linear U -> V} := [linear of 0].
(* lmodType somehow does not satisfy Scale.law by def *)
Program Definition linear_neg u : {linear U -> V} := GRing.opp_fun_linear u _.
Next Obligation. move=> _. apply/GRing.Scale.scale_law. Qed.
Definition linear_add u v := [linear of u \+ v].

Lemma linear_eq u v : (u: U -> V) = v -> u = v.
Proof. case: u v => [u +] [v +] /= Eq.
rewrite -{}Eq=> Hu Hu'. by have ->: Hu = Hu'.
Qed.

Lemma linear_assoc : associative linear_add.
Proof. move=> u v w. apply/linear_eq. case: u v w => [u _] [v _] [w _] /=. apply/addrA. Qed.

Lemma linear_comm : commutative linear_add.
Proof. move=> u v. apply/linear_eq. case: u v => [u _] [v _] /=. apply/addrC. Qed.

Lemma linear_add0r : left_id linear_zero linear_add.
Proof. move=> u. apply/linear_eq. case: u => [u _] /=. apply/add0r. Qed.

Lemma linear_addNr: left_inverse linear_zero linear_neg linear_add.
Proof. move=> u. apply/linear_eq. case: u => [u _] /=. apply/addNr. Qed.

Definition linear_zmodMixin := ZmodMixin linear_assoc linear_comm linear_add0r linear_addNr.
Canonical linear_zmodType := ZmodType {linear U -> V} linear_zmodMixin.

End LinearZmod.

Section LinearLmod.
Context {R: comRingType} (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).

Definition linear_scale (c: R) u := [linear of c \*: u].

Lemma linear_scalerA a b v : linear_scale a (linear_scale b v) = linear_scale (a * b) v.
Proof. apply/linear_eq. case: v=> [v _] /=. apply/scalerA. Qed.

Lemma linear_scale1r : left_id 1 linear_scale.
Proof. move=> v. apply/linear_eq. case: v=> [v _] /=. apply/scale1r. Qed.

Lemma linear_scalerDr : right_distributive linear_scale +%R.
Proof. move=> c u v. apply/linear_eq. case: u v=> [u _] [v _] /=. apply/scalerDr. Qed.

Lemma linear_scalerDl v : {morph linear_scale^~ v: a b / a + b}.
Proof. move=> a b. apply/linear_eq. case: v=> [v _] /=. apply/scalerDl. Qed.

Definition linear_lmodMixin := LmodMixin linear_scalerA linear_scale1r linear_scalerDr linear_scalerDl.
Canonical linear_lmodType := LmodType R {linear U -> V} linear_lmodMixin.

End LinearLmod.

Section BoundedSpace.
Context {R: realType} (U V: normedModType R).
Implicit Types (phUV: phant (U -> V)).

Definition linear_conti v :=
  v \in [set w: {linear U -> V} | {for 0, continuous w}].
Fact linear_conti_key: pred_key linear_conti. Proof. by []. Qed.
Canonical linear_conti_keyed := KeyedPred linear_conti_key.

Fact linear_conti_submod_closed : submod_closed linear_conti.
Proof. split.
- rewrite in_setE /=. apply/cst_continuous.
- move=> c u v. rewrite !in_setE /= => Hu Hv.
  by apply/continuousD; [apply/continuousZr|].
Qed.

Canonical linear_conti_opprPred := OpprPred linear_conti_submod_closed.
Canonical linear_conti_addrPred := AddrPred linear_conti_submod_closed.
Canonical linear_conti_zmodPred := ZmodPred linear_conti_submod_closed.
Canonical linear_conti_submodPred := SubmodPred linear_conti_submod_closed.

Inductive Bounded phUV: predArgType :=
  BoundedOp (u: {linear U -> V}) & u \in linear_conti.
Definition bdval phUV (u: Bounded phUV) := let: BoundedOp u' _ := u in u'.

Coercion bdval: Bounded >-> GRing.Linear.map.

Canonical bounded_subType phUV := Eval hnf in [subType for (@bdval phUV)].
Definition bounded_eqMixin phUV := Eval hnf in [eqMixin of Bounded phUV by <:].
Canonical bounded_eqType phUV := Eval hnf in EqType (Bounded phUV) (bounded_eqMixin phUV).
Definition bounded_choiceMixin phUV := [choiceMixin of (Bounded phUV) by <:].
Canonical bounded_choiceType phUV := ChoiceType (Bounded phUV) (bounded_choiceMixin phUV).

Definition bounded_zmodMixin phUV := [zmodMixin of Bounded phUV by <:].
Canonical bounded_zmodType phUV := ZmodType (Bounded phUV) (bounded_zmodMixin phUV).
Definition bounded_lmodMixin phUV := [lmodMixin of Bounded phUV by <:].
Canonical bounded_lmodType phUV := LmodType R (Bounded phUV) (bounded_lmodMixin phUV).

End BoundedSpace.

Module BoundedNorm.
Section BoundedNorm.
Context {R: realType} (U V: normedModType R) (phUV: phant (U -> V)).
Local Notation BoundedT := (Bounded U V phUV).
Implicit Types (u v : BoundedT).

(* Note: division by 0 is defined as 0, we leverage that fact. *)

Definition norm_ratio u x := `|u x| / `|x|.
Definition norm_range u := range (norm_ratio u).

Lemma norm_range_nonempty u : norm_range u !=set0.
Proof. exists (norm_ratio u 0). apply/imageT. Qed.

(* The norm indeed exists *)
Lemma norm_exists u : has_sup (norm_range u).
Proof.
split; first apply/norm_range_nonempty.
move: u=> [u]. rewrite /norm_range /norm_ratio /= in_setE /=.
move=> /linear_continuous0 /linear_boundedP /pinfty_ex_gt0 [M M0 HM].
exists M=> m /= [x _] <-.
have := normr_ge0 x. rewrite le_eqVlt=> /orP [/eqP <- | Cmp].
- by rewrite invr0 mulr0 ltW.
- by rewrite ler_pdivr_mulr.
Qed.

Definition norm u : R := sup (norm_range u).

Lemma norm_ub u x : norm_ratio u x <= norm u.
Proof. apply/sup_ub. by have [] := norm_exists u. apply/imageT. Qed.

Lemma normD u v : norm (u + v) <= norm u + norm v.
Proof.
apply/sup_le_ub; first apply/norm_range_nonempty.
move=> _ [x _ <-].
have H: norm_ratio (u + v) x <= norm_ratio u x + norm_ratio v x.
- by rewrite /norm_ratio -mulrDl ler_wpmul2r // ler_norm_add.
apply/le_trans; [apply/H|]. by rewrite ler_add // norm_ub.
Qed.

Lemma norm_eq0 u : norm u = 0 -> u = 0.
Proof.
move=> H. apply/val_inj/linear_eq/funext=> x /=.
have /eqP : norm_ratio u x = 0.
- apply/eqP; by rewrite eq_le -{1}H norm_ub /norm_ratio divr_ge0.
rewrite /norm_ratio mulf_eq0.
move => /orP [| /ltac: (rewrite invr_eq0)] /eqP/normr0_eq0 //.
move=> ->. apply/linear0.
Qed.

Lemma normmZ c v : norm (c *: v) = `|c| * norm v.
Proof.
rewrite /norm -mul_sup_eq //; last by apply/norm_exists. f_equal.
rewrite /norm_range image_comp. f_equal.
apply/funext=> x /=. by rewrite /norm_ratio normmZ /= mulrA.
Qed.

Lemma normrMn v n : norm (v *+ n) = norm v *+ n.
Proof.
rewrite -[v *+ n]scaler_nat -[norm v *+ n]scaler_nat.
have {2}-> : (n%:R : R) = `|n%:R| by apply/esym/ger0_norm.
apply/normmZ.
Qed.

Lemma normrN v : norm (- v) = norm v.
rewrite /norm. f_equal. rewrite /norm_range. f_equal.
apply/funext=> x. by rewrite /norm_ratio /= normrN.
Qed.

Definition normedZmodMixin :=
  Num.NormedMixin normD norm_eq0 normrMn normrN.
Canonical normedZmodType := NormedZmodType R BoundedT normedZmodMixin.

(* TODO Needs pseudometric space. Heck *)

Definition pointedDef := pointed_of_zmodule [zmodType of BoundedT].
Canonical pointedType := [pointedType of BoundedT for pointedDef].
Definition filteredDef := filtered_of_normedZmod [normedZmodType R of BoundedT].
Canonical filteredType := [filteredType BoundedT of BoundedT for filteredDef].

Definition pseudoMetricMixin :=
  @pseudoMetric_of_normedDomain R [normedZmodType R of BoundedT].
Program Definition uniformMixin := uniformityOfBallMixin
  (@nbhs_ball_normE _ [normedZmodType R of BoundedT]) pseudoMetricMixin.
Definition topologicalMixin := topologyOfEntourageMixin uniformMixin.

Canonical topologicalType := TopologicalType BoundedT topologicalMixin.
Canonical uniformType := UniformType BoundedT uniformMixin.
Canonical psudoMetricType := PseudoMetricType BoundedT pseudoMetricMixin.

Program Definition pseudoMetricNormedZmoduleMixin :=
  @PseudoMetricNormedZmodule.Mixin R [normedZmodType R of BoundedT] _ pseudoMetricMixin _.
Next Obligation. simpl. f_equal. Qed.
Canonical pseudoMetricNormedZmodType :=
  PseudoMetricNormedZmodType R BoundedT pseudoMetricNormedZmoduleMixin.

Definition normedModMixin := NormedModMixin normmZ.
Canonical normedModType := NormedModType R BoundedT normedModMixin.

End BoundedNorm.

Module Exports.
Canonical pointedType.
Canonical filteredType.
Canonical topologicalType.
Canonical uniformType.
Canonical psudoMetricType.
Canonical pseudoMetricNormedZmodType.
Canonical normedModType.
End Exports.
End BoundedNorm.
Export BoundedNorm.Exports.

Notation "{ 'bounded' fUV }" := (Bounded _ _ (Phant fUV)).
Notation BddLinear bdd := (BoundedOp (Phant _) _ bdd).

Section BoundedTheory.
Context (R: realType) (U V W: normedModType R).

Lemma comp_is_bounded
  (u: {bounded U -> V}) (v: {bounded V -> W}) : linear_conti [linear of v \o u].
Proof.
move: u v=> [u +] [v +] /=. rewrite !in_setE /= => Hu Hv.
by apply/continuous_comp; [| rewrite linear0].
Qed.

Definition comp_bounded u v := BddLinear (comp_is_bounded u v).

End BoundedTheory.