src/HOL/Analysis/Bounded_Linear_Function.thy
author paulson <lp15@cam.ac.uk>
Wed, 28 Sep 2016 17:01:01 +0100
changeset 63952 354808e9f44b
parent 63938 f6ce08859d4c
child 64267 b9a1486e79be
permissions -rw-r--r--
new material connected with HOL Light measure theory, plus more rationalisation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63627
6ddb43c6b711 rename HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl
parents: 63040
diff changeset
     1
(*  Title:      HOL/Analysis/Bounded_Linear_Function.thy
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     2
    Author:     Fabian Immler, TU München
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     3
*)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     4
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
     5
section \<open>Bounded Linear Function\<close>
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     6
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     7
theory Bounded_Linear_Function
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     8
imports
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
     9
  Topology_Euclidean_Space
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    10
  Operator_Norm
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    11
begin
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    12
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
    13
subsection \<open>Intro rules for @{term bounded_linear}\<close>
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    14
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    15
named_theorems bounded_linear_intros
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    16
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    17
lemma onorm_inner_left:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    18
  assumes "bounded_linear r"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    19
  shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    20
proof (rule onorm_bound)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    21
  fix x
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    22
  have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    23
    by (simp add: Cauchy_Schwarz_ineq2)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    24
  also have "\<dots> \<le> onorm r * norm x * norm f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    25
    by (intro mult_right_mono onorm assms norm_ge_zero)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    26
  finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    27
    by (simp add: ac_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    28
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    29
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    30
lemma onorm_inner_right:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    31
  assumes "bounded_linear r"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    32
  shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    33
  apply (subst inner_commute)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    34
  apply (rule onorm_inner_left[OF assms, THEN order_trans])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    35
  apply simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    36
  done
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    37
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    38
lemmas [bounded_linear_intros] =
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    39
  bounded_linear_zero
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    40
  bounded_linear_add
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    41
  bounded_linear_const_mult
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    42
  bounded_linear_mult_const
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    43
  bounded_linear_scaleR_const
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    44
  bounded_linear_const_scaleR
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    45
  bounded_linear_ident
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    46
  bounded_linear_setsum
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    47
  bounded_linear_Pair
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    48
  bounded_linear_sub
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    49
  bounded_linear_fst_comp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    50
  bounded_linear_snd_comp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    51
  bounded_linear_inner_left_comp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    52
  bounded_linear_inner_right_comp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    53
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    54
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    55
subsection \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    56
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    57
attribute_setup bounded_linear =
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    58
  \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    59
    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    60
      [
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    61
        (@{thm bounded_linear.has_derivative}, @{named_theorems derivative_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    62
        (@{thm bounded_linear.tendsto}, @{named_theorems tendsto_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    63
        (@{thm bounded_linear.continuous}, @{named_theorems continuous_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    64
        (@{thm bounded_linear.continuous_on}, @{named_theorems continuous_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    65
        (@{thm bounded_linear.uniformly_continuous_on}, @{named_theorems continuous_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    66
        (@{thm bounded_linear_compose}, @{named_theorems bounded_linear_intros})
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    67
      ]))\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    68
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    69
attribute_setup bounded_bilinear =
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    70
  \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    71
    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    72
      [
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    73
        (@{thm bounded_bilinear.FDERIV}, @{named_theorems derivative_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    74
        (@{thm bounded_bilinear.tendsto}, @{named_theorems tendsto_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    75
        (@{thm bounded_bilinear.continuous}, @{named_theorems continuous_intros}),
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    76
        (@{thm bounded_bilinear.continuous_on}, @{named_theorems continuous_intros}),
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    77
        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    78
          @{named_theorems bounded_linear_intros}),
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    79
        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    80
          @{named_theorems bounded_linear_intros}),
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    81
        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    82
          @{named_theorems continuous_intros}),
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    83
        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
62311
73bebf642d3b more antiquotations;
wenzelm
parents: 62127
diff changeset
    84
          @{named_theorems continuous_intros})
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    85
      ]))\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    86
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    87
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    88
subsection \<open>type of bounded linear functions\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    89
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    90
typedef (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    91
  "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    92
  morphisms blinfun_apply Blinfun
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    93
  by (blast intro: bounded_linear_intros)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    94
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    95
declare [[coercion
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    96
    "blinfun_apply :: ('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b"]]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    97
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    98
lemma bounded_linear_blinfun_apply[bounded_linear_intros]:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
    99
  "bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. blinfun_apply f (g x))"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   100
  by (metis blinfun_apply mem_Collect_eq bounded_linear_compose)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   101
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   102
setup_lifting type_definition_blinfun
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   103
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   104
lemma blinfun_eqI: "(\<And>i. blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   105
  by transfer auto
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   106
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   107
lemma bounded_linear_Blinfun_apply: "bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   108
  by (auto simp: Blinfun_inverse)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   109
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   110
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   111
subsection \<open>type class instantiations\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   112
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   113
instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   114
begin
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   115
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   116
lift_definition norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   117
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   118
lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   119
  is "\<lambda>f g x. f x - g x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   120
  by (rule bounded_linear_sub)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   121
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   122
definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   123
  where "dist_blinfun a b = norm (a - b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   124
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   125
definition [code del]:
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   126
  "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   127
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   128
definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   129
  where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   130
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   131
lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   132
  by (rule bounded_linear_minus)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   133
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   134
lift_definition zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   135
  by (rule bounded_linear_zero)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   136
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   137
lift_definition plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   138
  is "\<lambda>f g x. f x + g x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   139
  by (metis bounded_linear_add)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   140
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   141
lift_definition scaleR_blinfun::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>r f x. r *\<^sub>R f x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   142
  by (metis bounded_linear_compose bounded_linear_scaleR_right)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   143
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   144
definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   145
  where "sgn_blinfun x = scaleR (inverse (norm x)) x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   146
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   147
instance
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   148
  apply standard
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   149
  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61975
diff changeset
   150
  apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   151
  done
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   152
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   153
end
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   154
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   155
declare uniformity_Abort[where 'a="('a :: real_normed_vector) \<Rightarrow>\<^sub>L ('b :: real_normed_vector)", code]
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   156
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   157
lemma norm_blinfun_eqI:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   158
  assumes "n \<le> norm (blinfun_apply f x) / norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   159
  assumes "\<And>x. norm (blinfun_apply f x) \<le> n * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   160
  assumes "0 \<le> n"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   161
  shows "norm f = n"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   162
  by (auto simp: norm_blinfun_def
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   163
    intro!: antisym onorm_bound assms order_trans[OF _ le_onorm]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   164
    bounded_linear_intros)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   165
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   166
lemma norm_blinfun: "norm (blinfun_apply f x) \<le> norm f * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   167
  by transfer (rule onorm)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   168
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   169
lemma norm_blinfun_bound: "0 \<le> b \<Longrightarrow> (\<And>x. norm (blinfun_apply f x) \<le> b * norm x) \<Longrightarrow> norm f \<le> b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   170
  by transfer (rule onorm_bound)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   171
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   172
lemma bounded_bilinear_blinfun_apply[bounded_bilinear]: "bounded_bilinear blinfun_apply"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   173
proof
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   174
  fix f g::"'a \<Rightarrow>\<^sub>L 'b" and a b::'a and r::real
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   175
  show "(f + g) a = f a + g a" "(r *\<^sub>R f) a = r *\<^sub>R f a"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   176
    by (transfer, simp)+
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   177
  interpret bounded_linear f for f::"'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   178
    by (auto intro!: bounded_linear_intros)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   179
  show "f (a + b) = f a + f b" "f (r *\<^sub>R a) = r *\<^sub>R f a"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   180
    by (simp_all add: add scaleR)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   181
  show "\<exists>K. \<forall>a b. norm (blinfun_apply a b) \<le> norm a * norm b * K"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   182
    by (auto intro!: exI[where x=1] norm_blinfun)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   183
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   184
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   185
interpretation blinfun: bounded_bilinear blinfun_apply
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   186
  by (rule bounded_bilinear_blinfun_apply)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   187
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   188
lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   189
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   190
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   191
context bounded_bilinear
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   192
begin
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   193
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   194
named_theorems bilinear_simps
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   195
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   196
lemmas [bilinear_simps] =
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   197
  add_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   198
  add_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   199
  diff_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   200
  diff_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   201
  minus_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   202
  minus_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   203
  scaleR_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   204
  scaleR_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   205
  zero_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   206
  zero_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   207
  setsum_left
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   208
  setsum_right
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   209
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   210
end
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   211
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   212
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   213
instance blinfun :: (banach, banach) banach
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   214
proof
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   215
  fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   216
  assume "Cauchy X"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   217
  {
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   218
    fix x::'a
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   219
    {
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   220
      fix x::'a
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   221
      assume "norm x \<le> 1"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   222
      have "Cauchy (\<lambda>n. X n x)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   223
      proof (rule CauchyI)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   224
        fix e::real
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   225
        assume "0 < e"
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   226
        from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   227
          where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   228
          by auto
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   229
        show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   230
        proof (safe intro!: exI[where x=M])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   231
          fix m n
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   232
          assume le: "M \<le> m" "M \<le> n"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   233
          have "norm (X m x - X n x) = norm ((X m - X n) x)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   234
            by (simp add: blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   235
          also have "\<dots> \<le> norm (X m - X n) * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   236
             by (rule norm_blinfun)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   237
          also have "\<dots> \<le> norm (X m - X n) * 1"
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   238
            using \<open>norm x \<le> 1\<close> norm_ge_zero by (rule mult_left_mono)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   239
          also have "\<dots> = norm (X m - X n)" by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   240
          also have "\<dots> < e" using le by fact
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   241
          finally show "norm (X m x - X n x) < e" .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   242
        qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   243
      qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   244
      hence "convergent (\<lambda>n. X n x)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   245
        by (metis Cauchy_convergent_iff)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   246
    } note convergent_norm1 = this
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62963
diff changeset
   247
    define y where "y = x /\<^sub>R norm x"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   248
    have y: "norm y \<le> 1" and xy: "x = norm x *\<^sub>R y"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   249
      by (simp_all add: y_def inverse_eq_divide)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   250
    have "convergent (\<lambda>n. norm x *\<^sub>R X n y)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   251
      by (intro bounded_bilinear.convergent[OF bounded_bilinear_scaleR] convergent_const
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   252
        convergent_norm1 y)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   253
    also have "(\<lambda>n. norm x *\<^sub>R X n y) = (\<lambda>n. X n x)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   254
      by (subst xy) (simp add: blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   255
    finally have "convergent (\<lambda>n. X n x)" .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   256
  }
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   257
  then obtain v where v: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> v x"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   258
    unfolding convergent_def
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   259
    by metis
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   260
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   261
  have "Cauchy (\<lambda>n. norm (X n))"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   262
  proof (rule CauchyI)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   263
    fix e::real
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   264
    assume "e > 0"
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   265
    from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   266
      where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   267
      by auto
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   268
    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   269
    proof (safe intro!: exI[where x=M])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   270
      fix m n assume mn: "m \<ge> M" "n \<ge> M"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   271
      have "norm (norm (X m) - norm (X n)) \<le> norm (X m - X n)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   272
        by (metis norm_triangle_ineq3 real_norm_def)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   273
      also have "\<dots> < e" using mn by fact
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   274
      finally show "norm (norm (X m) - norm (X n)) < e" .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   275
    qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   276
  qed
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   277
  then obtain K where K: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow> K"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   278
    unfolding Cauchy_convergent_iff convergent_def
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   279
    by metis
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   280
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   281
  have "bounded_linear v"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   282
  proof
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   283
    fix x y and r::real
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   284
    from tendsto_add[OF v[of x] v [of y]] v[of "x + y", unfolded blinfun.bilinear_simps]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   285
      tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *\<^sub>R x", unfolded blinfun.bilinear_simps]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   286
    show "v (x + y) = v x + v y" "v (r *\<^sub>R x) = r *\<^sub>R v x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   287
      by (metis (poly_guards_query) LIMSEQ_unique)+
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   288
    show "\<exists>K. \<forall>x. norm (v x) \<le> norm x * K"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   289
    proof (safe intro!: exI[where x=K])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   290
      fix x
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   291
      have "norm (v x) \<le> K * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   292
        by (rule tendsto_le[OF _ tendsto_mult[OF K tendsto_const] tendsto_norm[OF v]])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   293
          (auto simp: norm_blinfun)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   294
      thus "norm (v x) \<le> norm x * K"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   295
        by (simp add: ac_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   296
    qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   297
  qed
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   298
  hence Bv: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> Blinfun v x"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   299
    by (auto simp: bounded_linear_Blinfun_apply v)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   300
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   301
  have "X \<longlonglongrightarrow> Blinfun v"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   302
  proof (rule LIMSEQ_I)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   303
    fix r::real assume "r > 0"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62963
diff changeset
   304
    define r' where "r' = r / 2"
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   305
    have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   306
    from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   307
    obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   308
      by metis
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   309
    show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   310
    proof (safe intro!: exI[where x=M])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   311
      fix n assume n: "M \<le> n"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   312
      have "norm (X n - Blinfun v) \<le> r'"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   313
      proof (rule norm_blinfun_bound)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   314
        fix x
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   315
        have "eventually (\<lambda>m. m \<ge> M) sequentially"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   316
          by (metis eventually_ge_at_top)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   317
        hence ev_le: "eventually (\<lambda>m. norm (X n x - X m x) \<le> r' * norm x) sequentially"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   318
        proof eventually_elim
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   319
          case (elim m)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   320
          have "norm (X n x - X m x) = norm ((X n - X m) x)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   321
            by (simp add: blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   322
          also have "\<dots> \<le> norm ((X n - X m)) * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   323
            by (rule norm_blinfun)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   324
          also have "\<dots> \<le> r' * norm x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   325
            using M[OF n elim] by (simp add: mult_right_mono)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   326
          finally show ?case .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   327
        qed
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   328
        have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   329
          by (auto intro!: tendsto_intros Bv)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   330
        show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
63952
354808e9f44b new material connected with HOL Light measure theory, plus more rationalisation
paulson <lp15@cam.ac.uk>
parents: 63938
diff changeset
   331
          by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   332
      qed (simp add: \<open>0 < r'\<close> less_imp_le)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   333
      thus "norm (X n - Blinfun v) < r"
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   334
        by (metis \<open>r' < r\<close> le_less_trans)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   335
    qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   336
  qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   337
  thus "convergent X"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   338
    by (rule convergentI)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   339
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   340
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   341
subsection \<open>On Euclidean Space\<close>
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   342
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   343
lemma Zfun_setsum:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   344
  assumes "finite s"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   345
  assumes f: "\<And>i. i \<in> s \<Longrightarrow> Zfun (f i) F"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   346
  shows "Zfun (\<lambda>x. setsum (\<lambda>i. f i x) s) F"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   347
  using assms by induct (auto intro!: Zfun_zero Zfun_add)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   348
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   349
lemma norm_blinfun_euclidean_le:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   350
  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   351
  shows "norm a \<le> setsum (\<lambda>x. norm (a x)) Basis"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   352
  apply (rule norm_blinfun_bound)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   353
   apply (simp add: setsum_nonneg)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   354
  apply (subst euclidean_representation[symmetric, where 'a='a])
63918
6bf55e6e0b75 left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63627
diff changeset
   355
  apply (simp only: blinfun.bilinear_simps setsum_distrib_right)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   356
  apply (rule order.trans[OF norm_setsum setsum_mono])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   357
  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   358
  done
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   359
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   360
lemma tendsto_componentwise1:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   361
  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   362
    and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   363
  assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) \<longlongrightarrow> a j) F)"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   364
  shows "(b \<longlongrightarrow> a) F"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   365
proof -
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   366
  have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x j - a j)) F"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   367
    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   368
  hence "Zfun (\<lambda>x. \<Sum>j\<in>Basis. norm (b x j - a j)) F"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   369
    by (auto intro!: Zfun_setsum)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   370
  thus ?thesis
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   371
    unfolding tendsto_Zfun_iff
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   372
    by (rule Zfun_le)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   373
      (auto intro!: order_trans[OF norm_blinfun_euclidean_le] simp: blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   374
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   375
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   376
lift_definition
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   377
  blinfun_of_matrix::"('b::euclidean_space \<Rightarrow> 'a::euclidean_space \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   378
  is "\<lambda>a x. \<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   379
  by (intro bounded_linear_intros)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   380
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   381
lemma blinfun_of_matrix_works:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   382
  fixes f::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   383
  shows "blinfun_of_matrix (\<lambda>i j. (f j) \<bullet> i) = f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   384
proof (transfer, rule,  rule euclidean_eqI)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   385
  fix f::"'a \<Rightarrow> 'b" and x::'a and b::'b assume "bounded_linear f" and b: "b \<in> Basis"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   386
  then interpret bounded_linear f by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   387
  have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   388
    = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   389
    using b
62390
842917225d56 more canonical names
nipkow
parents: 62311
diff changeset
   390
    by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: if_split intro!: setsum.cong)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   391
  also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   392
    using b by (simp add: setsum.delta)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   393
  also have "\<dots> = f x \<bullet> b"
63938
f6ce08859d4c More mainly topological results
paulson <lp15@cam.ac.uk>
parents: 63918
diff changeset
   394
    by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   395
  finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" .
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   396
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   397
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   398
lemma blinfun_of_matrix_apply:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   399
  "blinfun_of_matrix a x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   400
  by transfer simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   401
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   402
lemma blinfun_of_matrix_minus: "blinfun_of_matrix x - blinfun_of_matrix y = blinfun_of_matrix (x - y)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   403
  by transfer (auto simp: algebra_simps setsum_subtractf)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   404
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   405
lemma norm_blinfun_of_matrix:
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61916
diff changeset
   406
  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   407
  apply (rule norm_blinfun_bound)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   408
   apply (simp add: setsum_nonneg)
63918
6bf55e6e0b75 left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 63627
diff changeset
   409
  apply (simp only: blinfun_of_matrix_apply setsum_distrib_right)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   410
  apply (rule order_trans[OF norm_setsum setsum_mono])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   411
  apply (rule order_trans[OF norm_setsum setsum_mono])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   412
  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   413
  done
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   414
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   415
lemma tendsto_blinfun_of_matrix:
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   416
  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) \<longlongrightarrow> a i j) F"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   417
  shows "((\<lambda>n. blinfun_of_matrix (b n)) \<longlongrightarrow> blinfun_of_matrix a) F"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   418
proof -
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   419
  have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   420
    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61916
diff changeset
   421
  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   422
    by (auto intro!: Zfun_setsum)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   423
  thus ?thesis
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   424
    unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   425
    by (rule Zfun_le) (auto intro!: order_trans[OF norm_blinfun_of_matrix])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   426
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   427
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   428
lemma tendsto_componentwise:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   429
  fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   430
    and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   431
  shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) \<longlongrightarrow> a j \<bullet> i) F) \<Longrightarrow> (b \<longlongrightarrow> a) F"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   432
  apply (subst blinfun_of_matrix_works[of a, symmetric])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   433
  apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   434
  by (rule tendsto_blinfun_of_matrix)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   435
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   436
lemma
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   437
  continuous_blinfun_componentwiseI:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   438
  fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::euclidean_space"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   439
  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. (f x) j \<bullet> i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   440
  shows "continuous F f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   441
  using assms by (auto simp: continuous_def intro!: tendsto_componentwise)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   442
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   443
lemma
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   444
  continuous_blinfun_componentwiseI1:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   445
  fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   446
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. f x i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   447
  shows "continuous F f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   448
  using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   449
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   450
lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   451
  by (auto intro!: bounded_linearI' bounded_linear_intros)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   452
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   453
lemma continuous_blinfun_matrix:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   454
  fixes f:: "'b::t2_space \<Rightarrow> 'a::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   455
  assumes "continuous F f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   456
  shows "continuous F (\<lambda>x. (f x) j \<bullet> i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   457
  by (rule bounded_linear.continuous[OF bounded_linear_blinfun_matrix assms])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   458
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   459
lemma continuous_on_blinfun_matrix:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   460
  fixes f::"'a::t2_space \<Rightarrow> 'b::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   461
  assumes "continuous_on S f"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   462
  shows "continuous_on S (\<lambda>x. (f x) j \<bullet> i)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   463
  using assms
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   464
  by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   465
62963
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   466
lemma continuous_on_blinfun_of_matrix[continuous_intros]:
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   467
  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>s. g s i j)"
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   468
  shows "continuous_on S (\<lambda>s. blinfun_of_matrix (g s))"
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   469
  using assms
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   470
  by (auto simp: continuous_on intro!: tendsto_blinfun_of_matrix)
2d5eff9c3baa added rule
immler
parents: 62951
diff changeset
   471
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   472
lemma mult_if_delta:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   473
  "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   474
  by auto
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   475
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   476
lemma compact_blinfun_lemma:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   477
  fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   478
  assumes "bounded (range f)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   479
  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   480
    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
62127
d8e7738bd2e9 generalized proofs
immler
parents: 62102
diff changeset
   481
  by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
d8e7738bd2e9 generalized proofs
immler
parents: 62102
diff changeset
   482
   (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
d8e7738bd2e9 generalized proofs
immler
parents: 62102
diff changeset
   483
    simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta setsum.delta'
d8e7738bd2e9 generalized proofs
immler
parents: 62102
diff changeset
   484
      scaleR_setsum_left[symmetric])
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   485
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   486
lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   487
  apply (auto intro!: blinfun_eqI)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   488
  apply (subst (2) euclidean_representation[symmetric, where 'a='a])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   489
  apply (subst (1) euclidean_representation[symmetric, where 'a='a])
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   490
  apply (simp add: blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   491
  done
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   492
62951
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   493
lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)"
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   494
  by (intro blinfun_euclidean_eqI)
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   495
     (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   496
      cond_application_beta setsum.delta' euclidean_representation
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   497
      cong: if_cong)
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   498
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61973
diff changeset
   499
text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   500
instance blinfun :: (euclidean_space, euclidean_space) heine_borel
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   501
proof
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   502
  fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   503
  assume f: "bounded (range f)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   504
  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   505
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   506
    using compact_blinfun_lemma [OF f] by blast
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   507
  {
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   508
    fix e::real
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   509
    let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   510
    assume "e > 0"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   511
    hence "e / ?d > 0" by (simp add: DIM_positive)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   512
    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   513
      by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   514
    moreover
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   515
    {
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   516
      fix n
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   517
      assume n: "\<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   518
      have "norm (f (r n) - l) = norm (blinfun_of_matrix (\<lambda>i j. (f (r n) - l) j \<bullet> i))"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   519
        unfolding blinfun_of_matrix_works ..
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   520
      also note norm_blinfun_of_matrix
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   521
      also have "(\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) <
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   522
        (\<Sum>i\<in>(Basis::'b set). e / real_of_nat DIM('b))"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   523
      proof (rule setsum_strict_mono)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   524
        fix i::'b assume i: "i \<in> Basis"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   525
        have "(\<Sum>j::'a\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < (\<Sum>j::'a\<in>Basis. e / ?d)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   526
        proof (rule setsum_strict_mono)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   527
          fix j::'a assume j: "j \<in> Basis"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   528
          have "\<bar>(f (r n) - l) j \<bullet> i\<bar> \<le> norm ((f (r n) - l) j)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   529
            by (simp add: Basis_le_norm i)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   530
          also have "\<dots> < e / ?d"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   531
            using n i j by (auto simp: dist_norm blinfun.bilinear_simps)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   532
          finally show "\<bar>(f (r n) - l) j \<bullet> i\<bar> < e / ?d" by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   533
        qed simp_all
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   534
        also have "\<dots> \<le> e / real_of_nat DIM('b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   535
          by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   536
        finally show "(\<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < e / real_of_nat DIM('b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   537
          by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   538
      qed simp_all
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   539
      also have "\<dots> \<le> e" by simp
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   540
      finally have "dist (f (r n)) l < e"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   541
        by (auto simp: dist_norm)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   542
    }
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   543
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   544
      using eventually_elim2 by force
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   545
  }
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   546
  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   547
    unfolding o_def tendsto_iff by simp
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   548
  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   549
    by auto
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   550
qed
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   551
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   552
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   553
subsection \<open>concrete bounded linear functions\<close>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   554
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   555
lemma transfer_bounded_bilinear_bounded_linearI:
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   556
  assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   557
  shows "bounded_bilinear g = bounded_linear f"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   558
proof
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   559
  assume "bounded_bilinear g"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   560
  then interpret bounded_bilinear f by (simp add: assms)
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   561
  show "bounded_linear f"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   562
  proof (unfold_locales, safe intro!: blinfun_eqI)
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   563
    fix i
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   564
    show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   565
      by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   566
    from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   567
      by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq ac_simps)
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   568
  qed
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   569
qed (auto simp: assms intro!: blinfun.comp)
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   570
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   571
lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   572
  "(rel_fun (rel_fun op = (pcr_blinfun op = op =)) op =) bounded_bilinear bounded_linear"
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   573
  by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   574
    intro!: transfer_bounded_bilinear_bounded_linearI)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   575
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   576
context bounded_bilinear
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   577
begin
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   578
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   579
lift_definition prod_left::"'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'c" is "(\<lambda>b a. prod a b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   580
  by (rule bounded_linear_left)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   581
declare prod_left.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   582
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   583
lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   584
  by transfer (rule flip)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   585
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   586
lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   587
  by (rule bounded_linear_right)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   588
declare prod_right.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   589
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   590
lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   591
  by transfer (rule bounded_bilinear_axioms)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   592
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   593
end
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   594
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   595
lift_definition id_blinfun::"'a::real_normed_vector \<Rightarrow>\<^sub>L 'a" is "\<lambda>x. x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   596
  by (rule bounded_linear_ident)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   597
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   598
lemmas blinfun_apply_id_blinfun[simp] = id_blinfun.rep_eq
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   599
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   600
lemma norm_blinfun_id[simp]:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   601
  "norm (id_blinfun::'a::{real_normed_vector, perfect_space} \<Rightarrow>\<^sub>L 'a) = 1"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   602
  by transfer (auto simp: onorm_id)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   603
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   604
lemma norm_blinfun_id_le:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   605
  "norm (id_blinfun::'a::real_normed_vector \<Rightarrow>\<^sub>L 'a) \<le> 1"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   606
  by transfer (auto simp: onorm_id_le)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   607
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   608
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   609
lift_definition fst_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'a" is fst
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   610
  by (rule bounded_linear_fst)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   611
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   612
lemma blinfun_apply_fst_blinfun[simp]: "blinfun_apply fst_blinfun = fst"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   613
  by transfer (rule refl)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   614
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   615
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   616
lift_definition snd_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'b" is snd
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   617
  by (rule bounded_linear_snd)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   618
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   619
lemma blinfun_apply_snd_blinfun[simp]: "blinfun_apply snd_blinfun = snd"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   620
  by transfer (rule refl)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   621
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   622
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   623
lift_definition blinfun_compose::
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   624
  "'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   625
    'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   626
    'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "op o"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   627
  parametric comp_transfer
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   628
  unfolding o_def
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   629
  by (rule bounded_linear_compose)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   630
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   631
lemma blinfun_apply_blinfun_compose[simp]: "(a o\<^sub>L b) c = a (b c)"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   632
  by (simp add: blinfun_compose.rep_eq)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   633
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   634
lemma norm_blinfun_compose:
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   635
  "norm (f o\<^sub>L g) \<le> norm f * norm g"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   636
  by transfer (rule onorm_compose)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   637
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   638
lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear op o\<^sub>L"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   639
  by unfold_locales
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   640
    (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   641
62951
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   642
lemma blinfun_compose_zero[simp]:
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   643
  "blinfun_compose 0 = (\<lambda>_. 0)"
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   644
  "blinfun_compose x 0 = 0"
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   645
  by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
f59ef58f420b added lemmas
immler
parents: 62390
diff changeset
   646
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   647
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   648
lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   649
  by (rule bounded_linear_inner_right)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   650
declare blinfun_inner_right.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   651
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   652
lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   653
  by transfer (rule bounded_bilinear_inner)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   654
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   655
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   656
lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   657
  by (rule bounded_linear_inner_left)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   658
declare blinfun_inner_left.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   659
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   660
lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   661
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   662
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   663
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   664
lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   665
  by (rule bounded_linear_scaleR_right)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   666
declare blinfun_scaleR_right.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   667
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   668
lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   669
  by transfer (rule bounded_bilinear_scaleR)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   670
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   671
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   672
lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   673
  by (rule bounded_linear_scaleR_left)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   674
lemmas [simp] = blinfun_scaleR_left.rep_eq
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   675
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   676
lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   677
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   678
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   679
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   680
lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   681
  by (rule bounded_linear_mult_right)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   682
declare blinfun_mult_right.rep_eq[simp]
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   683
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   684
lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   685
  by transfer (rule bounded_bilinear_mult)
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   686
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   687
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   688
lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   689
  by (rule bounded_linear_mult_left)
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   690
lemmas [simp] = blinfun_mult_left.rep_eq
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   691
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   692
lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
61916
7950ae6d3266 transfer rule for bounded_linear of blinfun
immler
parents: 61915
diff changeset
   693
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   694
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
diff changeset
   695
end