Theory BoundedLinear

(*  Title       : BoundedLinear.thy
    ID          : $Id$
    Author      : Brian Huffman
*)

header {* Constructing Bounded Linear Operators *}

theory BoundedLinear
imports Lim
begin

lemma bounded_linear_zero: "bounded_linear (λx. 0)"
by (unfold_locales, rule_tac [3] x="0" in exI, simp_all)

lemma bounded_linear_ident: "bounded_linear (λx. x)"
by (unfold_locales, rule_tac [3] x="1" in exI, simp_all)

lemma bounded_linear_uminus: "bounded_linear uminus"
by (unfold_locales, rule_tac [3] x="1" in exI, simp_all)

lemma bounded_linear_compose:
  includes bounded_linear f
  includes bounded_linear g
  shows "bounded_linear (λx. f (g x))"
proof (unfold_locales)
  fix x y show "f (g (x + y)) = f (g x) + f (g y)"
    by (simp only: f.add g.add)
next
  fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
    by (simp only: f.scaleR g.scaleR)
next
  obtain Kf where f: "!!x. norm (f x) ≤ norm x * Kf" and Kf: "0 ≤ Kf"
    using f.nonneg_bounded by fast
  obtain Kg where g: "!!x. norm (g x) ≤ norm x * Kg"
    using g.bounded by fast
  show "∃K. ∀x. norm (f (g x)) ≤ norm x * K"
  proof (intro exI allI)
    fix x
    have "norm (f (g x)) ≤ norm (g x) * Kf"
      using f .
    also have "norm (g x) * Kf ≤ (norm x * Kg) * Kf"
      using g Kf by (rule mult_right_mono)
    finally show "norm (f (g x)) ≤ norm x * (Kg * Kf)"
      by (simp only: mult_assoc)
  qed
qed

lemma bounded_linear_o:
  "[|bounded_linear f; bounded_linear g|] ==> bounded_linear (f o g)"
unfolding o_def by (rule bounded_linear_compose)

lemma bounded_linear_add:
  includes bounded_linear f
  includes bounded_linear g
  shows "bounded_linear (λx. f x + g x)"
proof (unfold_locales)
  fix x y show "f (x + y) + g (x + y) = (f x + g x) + (f y + g y)"
    by (simp only: f.add g.add add_ac)
next
  fix r x show "f (scaleR r x) + g (scaleR r x) = scaleR r (f x + g x)"
    by (simp only: f.scaleR g.scaleR scaleR_right_distrib)
next
  obtain Kf where f: "!!x. norm (f x) ≤ norm x * Kf"
    using f.bounded by fast
  obtain Kg where g: "!!x. norm (g x) ≤ norm x * Kg"
    using g.bounded by fast
  show "∃K. ∀x. norm (f x + g x) ≤ norm x * K"
  proof (intro exI allI)
    fix x
    have "norm (f x + g x) ≤ norm (f x) + norm (g x)"
      by (rule norm_triangle_ineq)
    also have "norm (f x) + norm (g x) ≤ norm x * Kf + norm x * Kg"
      using f g by (rule add_mono)
    finally show "norm (f x + g x) ≤ norm x * (Kf + Kg)"
      by (simp only: right_distrib)
  qed
qed

lemma bounded_linear_minus:
  "bounded_linear f ==> bounded_linear (λx. - f x)"
by (rule bounded_linear_uminus [THEN bounded_linear_compose])

lemma bounded_linear_diff:
  "[|bounded_linear f; bounded_linear g|] ==> bounded_linear (λx. f x - g x)"
by (simp only: diff_minus bounded_linear_add bounded_linear_minus)

lemma bounded_linear_setsum:
  "∀i∈A. bounded_linear (f i) ==> bounded_linear (λx. ∑i∈A. f i x)"
apply (cases "finite A")
apply (erule rev_mp, erule finite_induct)
apply (simp add: bounded_linear_zero)
apply (simp add: bounded_linear_add)
apply (simp add: bounded_linear_zero)
done

lemmas bounded_linear_scaleR =
  scaleR.bounded_linear_right [THEN bounded_linear_compose]

lemmas bounded_linear_mult_const =
  mult.bounded_linear_left [THEN bounded_linear_compose]

lemmas bounded_linear_const_mult =
  mult.bounded_linear_right [THEN bounded_linear_compose]

end