Lemmas for functions bounded on a range

CHANGELOG_UNRELEASED.md

@@ -234,6 +234,15 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `normed_module.v`,
+  + new lemmas `bounded_rangeM`, `bounded_rangeMl`, `bounded_rangeMr`, and 
+    `bounded_range_max`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `bounded_range`, `bounded_rangeP`, `bounded_range_exP`, 
+    `bounded_range_setU`, `bounded_range_set0`, `bounded_range_set1`, 
+    `bounded_rangeW`, `bounded_rangeD`, `bounded_range_comp`, 
+    `bounded_range_shift`, `bounded_range_itv_tweak`, and `eq_bounded_range`.
+
 ### Changed
 
 - in `realsum.v`:

theories/normedtype_theory/normed_module.v

@@ -1918,6 +1918,51 @@ Lemma bounded_locally (T : topologicalType)
   [bounded f x | x in A] -> [locally [bounded f x | x in A]].
 Proof. by move=> /sub_boundedr AB x Ax; apply: AB; apply: within_nbhsW. Qed.
 
+Section bounded_range.
+Context (T : Type) (R : realFieldType).
+Implicit Types (f g : T -> R) (A : set T).
+
+Lemma bounded_rangeM f g A : 
+  [bounded f x | x in A] -> [bounded g x | x in A] -> [bounded f x * g x | x in A].
+Proof.
+move=> /bounded_range_exP[Mf Mf_gt0 Mf_ub] /bounded_range_exP[Mg Mg_gt0 Mg_ub].
+apply: bounded_rangeP => x Ax /=.
+rewrite normrM.
+apply: ler_pM => //.
+- by apply: Mf_ub.
+- by apply: Mg_ub.
+Qed.
+
+Lemma bounded_rangeMl f A (c : R) : [bounded f x | x in A] -> [bounded c * f x | x in A].
+Proof.
+  move=> bf.
+  apply: bounded_rangeM => //.
+  by exact: bounded_cst.
+Qed.
+
+Lemma bounded_rangeMr f A (c : R) : [bounded f x | x in A] -> [bounded f x * c | x in A].
+Proof.
+  move=> bf.
+  apply: bounded_rangeM => //.
+  by exact: bounded_cst.
+Qed.
+
+Lemma bounded_range_max f g A :
+  [bounded f x | x in A] ->
+  [bounded g x | x in A] ->
+  [bounded Num.max (f x) (g x) | x in A].
+Proof.
+  move=> /bounded_range_exP[Mf Mf_gt0 Mf_ub] /bounded_range_exP[Mg Mg_gt0 Mg_ub].
+  apply: (bounded_rangeP (M := Num.max Mf Mg)) => x Ax /=.
+  case: (leP (f x) (g x)) => _.
+  - apply: le_trans; first by apply: Mg_ub.
+    by rewrite le_max lexx orbT.
+  - apply: le_trans; first by apply: Mf_ub.
+    by rewrite le_max lexx.
+Qed.
+
+End bounded_range.
+
 Notation "k .-lipschitz_on f" :=
   (dominated_by (self_sub id) k (self_sub f)) : type_scope.
 

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1336,6 +1336,131 @@ Unshelve. all: by end_near. Qed.
 
 End bounded_near.
 
+Section bounded_range.
+Implicit Types (T : Type) (K : realFieldType).
+
+Lemma bounded_range T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (A : set T) : 
+  [bounded f x | x in A] <-> bounded_set (f @` A).
+Proof.
+split; rewrite /bounded_set /bounded_near.
+- move=> bf.
+  by near do move=> _ [+ + <-] /=.
+- move=> bif.
+  near=> M => x Ax /=.
+  have : globally (f @` A) [set x | `|x| <= M] by near: M.
+  by apply; exists x.
+Unshelve. all: by end_near.
+Qed.
+
+Lemma bounded_rangeP T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (A : set T) (M : K) :
+  (forall x, A x -> `|f x| <= M) -> [bounded f x | x in A].
+Proof.
+rewrite /bounded_near => M_ub.
+near=> M' => x Ax /=.
+apply: le_trans; first by apply: M_ub.
+near: M'.
+by apply: nbhs_pinfty_ge.
+Unshelve. all: by end_near.
+Qed.
+
+Lemma bounded_range_exP T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (A : set T) :
+  [bounded f x | x in A] <-> (exists2 M : K, M > 0 & forall x, A x -> `|f x| <= M).
+Proof.
+rewrite /bounded_near; split; first by move/pinfty_ex_gt0.
+move=> [M M_gt0 M_ub].
+near=> M' => x Ax.
+apply: le_trans; first by apply: M_ub.
+near: M'.
+apply: nbhs_pinfty_ge.
+by apply: gtr0_real.
+Unshelve. all: by end_near.
+Qed.  
+
+Lemma bounded_range_setU T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (A B : set T) :
+  [bounded f x | x in A] -> [bounded f x | x in B] -> [bounded f x | x in A `|` B]%classic.
+Proof.
+move=> /bounded_range_exP[MA MA_gt0 MA_ub] /bounded_range_exP[MB MB_gt0 MB_ub].
+apply: (bounded_rangeP (M := MA + MB)) => x [Ax|Bx].
+- apply: le_trans; first by apply: MA_ub.
+  by rewrite lerDl ltW.
+- apply: le_trans; first by apply: MB_ub.
+  by rewrite lerDr ltW.
+Qed. 
+
+Lemma bounded_range_set0 T K (V : pseudoMetricNormedZmodType K) (f : T -> V) : [bounded f x | x in set0].
+Proof.
+by near=> M => /=.
+Unshelve. all: by end_near. Qed.
+
+Lemma bounded_range_set1 T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (x0 : T) : [bounded f x | x in [set x0]].
+Proof. by apply: bounded_rangeP => ? ->. Qed.
+
+Hint Resolve bounded_range_set1 bounded_range_set0 : core.
+
+Lemma bounded_rangeW T K (V : pseudoMetricNormedZmodType K) (f : T -> V) (A B : set T) :
+  A `<=` B -> [bounded f x | x in B] -> [bounded f x | x in A].
+Proof.
+move=> A_sub_B /bounded_range_exP[M M_gt0 M_ub].
+apply: bounded_rangeP => x /A_sub_B.
+exact: M_ub.
+Qed.
+
+Lemma bounded_rangeD T K (V : pseudoMetricNormedZmodType K) (f g : T -> V) (A : set T) : 
+  [bounded f x | x in A] -> [bounded g x | x in A] -> [bounded f x + g x | x in A].
+Proof.
+move=> /bounded_range_exP[Mf Mf_gt0 Mf_ub] /bounded_range_exP[Mg Mg_gt0 Mg_ub].
+apply: bounded_rangeP.
+move=> x Ax /=.
+apply: le_trans; first by exact: ler_normD.
+apply: lerD.
+- by apply: Mf_ub. 
+- by apply: Mg_ub.
+Qed.
+
+Lemma bounded_range_comp (T U : Type) K (V : pseudoMetricNormedZmodType K) (f : T -> U) (g : U -> V) (E : set T) (F : set U) :
+  f @` E `<=` F ->
+  [bounded g y | y in F] -> [bounded g (f x) | x in E].
+Proof.
+move=> rng_sub /bounded_range_exP[Mg Mg_gt0 Mg_ub].
+apply: bounded_rangeP => x Ex.
+apply: Mg_ub.
+by apply: rng_sub; exists x.
+Qed.
+
+Lemma bounded_range_shift (T : numDomainType) K (V : pseudoMetricNormedZmodType K) (f : T -> V) (x y a : T) (b1 b2 : bool) :
+  [bounded f z | z in [set` Interval (BSide b1 (x - a)) (BSide b2 (y - a))]] ->
+  [bounded f (z - a) | z in [set` Interval (BSide b1 x) (BSide b2 y)]].
+Proof.
+apply: bounded_range_comp => ? [/= z + <-].
+rewrite /= !in_itv.
+by case: b1 b2 => [|] [|] /=; rewrite ?ltrD2r ?lerD2r.
+Qed.
+
+Lemma bounded_range_itv_tweak d (T : orderType d) K (V : pseudoMetricNormedZmodType K) (f : T -> V) (a b : T) (b1 b2 b1' b2' : bool) :
+  [bounded f x | x in [set` Interval (BSide b1 a) (BSide b2 b)]] -> [bounded f x | x in [set` Interval (BSide b1' a) (BSide b2' b)]].
+Proof.
+case: (leP a b) => [a_le_b|b_lt_a _]; last first.
+  rewrite set_itv_ge// -leNgt leBSide.
+  by apply: lteifS.
+move=> bf.
+apply: (bounded_rangeW (B := `[a, b])); first by (apply: subset_itv; rewrite bnd_simp).
+rewrite -(setUitv_set2 b1 b2)//.
+by apply/bounded_range_setU; last by apply/bounded_range_setU.
+Qed.
+
+Lemma eq_bounded_range T K (V : pseudoMetricNormedZmodType K) (f g : T -> V) (A : set T) :
+  {in A, f =1 g} -> [bounded f x | x in A] = [bounded g x | x in A].
+Proof.
+move=> eqfg.
+rewrite /bounded_near.
+apply: eq_near => M.
+apply/propeqP; apply: eq_forall => x.
+apply: eq_forall => Ax /=.
+by rewrite eqfg ?inE.
+Qed.
+
+End bounded_range.
+
 Section cvg_bounded.
 Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).