Theory Bounded_Linear_Function

theory Bounded_Linear_Function
imports Operator_Norm Uniform_Limit
(*  Title:      HOL/Analysis/Bounded_Linear_Function.thy
    Author:     Fabian Immler, TU M√ľnchen
*)

section ‹Bounded Linear Function›

theory Bounded_Linear_Function
imports
  Topology_Euclidean_Space
  Operator_Norm
  Uniform_Limit
begin

lemma onorm_componentwise:
  assumes "bounded_linear f"
  shows "onorm f ≤ (∑i∈Basis. norm (f i))"
proof -
  {
    fix i::'a
    assume "i ∈ Basis"
    hence "onorm (λx. (x ∙ i) *R f i) ≤ onorm (λx. (x ∙ i)) * norm (f i)"
      by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
    also have "… ≤  norm i * norm (f i)"
      by (rule mult_right_mono)
        (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
    finally have "onorm (λx. (x ∙ i) *R f i) ≤ norm (f i)" using ‹i ∈ Basis›
      by simp
  } hence "onorm (λx. ∑i∈Basis. (x ∙ i) *R f i) ≤ (∑i∈Basis. norm (f i))"
    by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
      sum_mono bounded_linear_inner_left)
  also have "(λx. ∑i∈Basis. (x ∙ i) *R f i) = (λx. f (∑i∈Basis. (x ∙ i) *R i))"
    by (simp add: linear_sum bounded_linear.linear assms linear_simps)
  also have "… = f"
    by (simp add: euclidean_representation)
  finally show ?thesis .
qed

lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]

subsection ‹Intro rules for @{term bounded_linear}›

named_theorems bounded_linear_intros

lemma onorm_inner_left:
  assumes "bounded_linear r"
  shows "onorm (λx. r x ∙ f) ≤ onorm r * norm f"
proof (rule onorm_bound)
  fix x
  have "norm (r x ∙ f) ≤ norm (r x) * norm f"
    by (simp add: Cauchy_Schwarz_ineq2)
  also have "… ≤ onorm r * norm x * norm f"
    by (intro mult_right_mono onorm assms norm_ge_zero)
  finally show "norm (r x ∙ f) ≤ onorm r * norm f * norm x"
    by (simp add: ac_simps)
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)

lemma onorm_inner_right:
  assumes "bounded_linear r"
  shows "onorm (λx. f ∙ r x) ≤ norm f * onorm r"
  apply (subst inner_commute)
  apply (rule onorm_inner_left[OF assms, THEN order_trans])
  apply simp
  done

lemmas [bounded_linear_intros] =
  bounded_linear_zero
  bounded_linear_add
  bounded_linear_const_mult
  bounded_linear_mult_const
  bounded_linear_scaleR_const
  bounded_linear_const_scaleR
  bounded_linear_ident
  bounded_linear_sum
  bounded_linear_Pair
  bounded_linear_sub
  bounded_linear_fst_comp
  bounded_linear_snd_comp
  bounded_linear_inner_left_comp
  bounded_linear_inner_right_comp


subsection ‹declaration of derivative/continuous/tendsto introduction rules for bounded linear functions›

attribute_setup bounded_linear =
  ‹Scan.succeed (Thm.declaration_attribute (fn thm =>
    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
      [
        (@{thm bounded_linear.has_derivative}, @{named_theorems derivative_intros}),
        (@{thm bounded_linear.tendsto}, @{named_theorems tendsto_intros}),
        (@{thm bounded_linear.continuous}, @{named_theorems continuous_intros}),
        (@{thm bounded_linear.continuous_on}, @{named_theorems continuous_intros}),
        (@{thm bounded_linear.uniformly_continuous_on}, @{named_theorems continuous_intros}),
        (@{thm bounded_linear_compose}, @{named_theorems bounded_linear_intros})
      ]))›

attribute_setup bounded_bilinear =
  ‹Scan.succeed (Thm.declaration_attribute (fn thm =>
    fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
      [
        (@{thm bounded_bilinear.FDERIV}, @{named_theorems derivative_intros}),
        (@{thm bounded_bilinear.tendsto}, @{named_theorems tendsto_intros}),
        (@{thm bounded_bilinear.continuous}, @{named_theorems continuous_intros}),
        (@{thm bounded_bilinear.continuous_on}, @{named_theorems continuous_intros}),
        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
          @{named_theorems bounded_linear_intros}),
        (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
          @{named_theorems bounded_linear_intros}),
        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
          @{named_theorems continuous_intros}),
        (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
          @{named_theorems continuous_intros})
      ]))›


subsection ‹type of bounded linear functions›

typedef (overloaded) ('a, 'b) blinfun ("(_ ⇒L /_)" [22, 21] 21) =
  "{f::'a::real_normed_vector⇒'b::real_normed_vector. bounded_linear f}"
  morphisms blinfun_apply Blinfun
  by (blast intro: bounded_linear_intros)

declare [[coercion
    "blinfun_apply :: ('a::real_normed_vector ⇒L'b::real_normed_vector) ⇒ 'a ⇒ 'b"]]

lemma bounded_linear_blinfun_apply[bounded_linear_intros]:
  "bounded_linear g ⟹ bounded_linear (λx. blinfun_apply f (g x))"
  by (metis blinfun_apply mem_Collect_eq bounded_linear_compose)

setup_lifting type_definition_blinfun

lemma blinfun_eqI: "(⋀i. blinfun_apply x i = blinfun_apply y i) ⟹ x = y"
  by transfer auto

lemma bounded_linear_Blinfun_apply: "bounded_linear f ⟹ blinfun_apply (Blinfun f) = f"
  by (auto simp: Blinfun_inverse)


subsection ‹type class instantiations›

instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
begin

lift_definition norm_blinfun :: "'a ⇒L 'b ⇒ real" is onorm .

lift_definition minus_blinfun :: "'a ⇒L 'b ⇒ 'a ⇒L 'b ⇒ 'a ⇒L 'b"
  is "λf g x. f x - g x"
  by (rule bounded_linear_sub)

definition dist_blinfun :: "'a ⇒L 'b ⇒ 'a ⇒L 'b ⇒ real"
  where "dist_blinfun a b = norm (a - b)"

definition [code del]:
  "(uniformity :: (('a ⇒L 'b) × ('a ⇒L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"

definition open_blinfun :: "('a ⇒L 'b) set ⇒ bool"
  where [code del]: "open_blinfun S = (∀x∈S. ∀F (x', y) in uniformity. x' = x ⟶ y ∈ S)"

lift_definition uminus_blinfun :: "'a ⇒L 'b ⇒ 'a ⇒L 'b" is "λf x. - f x"
  by (rule bounded_linear_minus)

lift_definition zero_blinfun :: "'a ⇒L 'b" is "λx. 0"
  by (rule bounded_linear_zero)

lift_definition plus_blinfun :: "'a ⇒L 'b ⇒ 'a ⇒L 'b ⇒ 'a ⇒L 'b"
  is "λf g x. f x + g x"
  by (metis bounded_linear_add)

lift_definition scaleR_blinfun::"real ⇒ 'a ⇒L 'b ⇒ 'a ⇒L 'b" is "λr f x. r *R f x"
  by (metis bounded_linear_compose bounded_linear_scaleR_right)

definition sgn_blinfun :: "'a ⇒L 'b ⇒ 'a ⇒L 'b"
  where "sgn_blinfun x = scaleR (inverse (norm x)) x"

instance
  apply standard
  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
  apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
  done

end

declare uniformity_Abort[where 'a="('a :: real_normed_vector) ⇒L ('b :: real_normed_vector)", code]

lemma norm_blinfun_eqI:
  assumes "n ≤ norm (blinfun_apply f x) / norm x"
  assumes "⋀x. norm (blinfun_apply f x) ≤ n * norm x"
  assumes "0 ≤ n"
  shows "norm f = n"
  by (auto simp: norm_blinfun_def
    intro!: antisym onorm_bound assms order_trans[OF _ le_onorm]
    bounded_linear_intros)

lemma norm_blinfun: "norm (blinfun_apply f x) ≤ norm f * norm x"
  by transfer (rule onorm)

lemma norm_blinfun_bound: "0 ≤ b ⟹ (⋀x. norm (blinfun_apply f x) ≤ b * norm x) ⟹ norm f ≤ b"
  by transfer (rule onorm_bound)

lemma bounded_bilinear_blinfun_apply[bounded_bilinear]: "bounded_bilinear blinfun_apply"
proof
  fix f g::"'a ⇒L 'b" and a b::'a and r::real
  show "(f + g) a = f a + g a" "(r *R f) a = r *R f a"
    by (transfer, simp)+
  interpret bounded_linear f for f::"'a ⇒L 'b"
    by (auto intro!: bounded_linear_intros)
  show "f (a + b) = f a + f b" "f (r *R a) = r *R f a"
    by (simp_all add: add scaleR)
  show "∃K. ∀a b. norm (blinfun_apply a b) ≤ norm a * norm b * K"
    by (auto intro!: exI[where x=1] norm_blinfun)
qed

interpretation blinfun: bounded_bilinear blinfun_apply
  by (rule bounded_bilinear_blinfun_apply)

lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left


context bounded_bilinear
begin

named_theorems bilinear_simps

lemmas [bilinear_simps] =
  add_left
  add_right
  diff_left
  diff_right
  minus_left
  minus_right
  scaleR_left
  scaleR_right
  zero_left
  zero_right
  sum_left
  sum_right

end


instance blinfun :: (real_normed_vector, banach) banach
proof
  fix X::"nat ⇒ 'a ⇒L 'b"
  assume "Cauchy X"
  {
    fix x::'a
    {
      fix x::'a
      assume "norm x ≤ 1"
      have "Cauchy (λn. X n x)"
      proof (rule CauchyI)
        fix e::real
        assume "0 < e"
        from CauchyD[OF ‹Cauchy X› ‹0 < e›] obtain M
          where M: "⋀m n. m ≥ M ⟹ n ≥ M ⟹ norm (X m - X n) < e"
          by auto
        show "∃M. ∀m≥M. ∀n≥M. norm (X m x - X n x) < e"
        proof (safe intro!: exI[where x=M])
          fix m n
          assume le: "M ≤ m" "M ≤ n"
          have "norm (X m x - X n x) = norm ((X m - X n) x)"
            by (simp add: blinfun.bilinear_simps)
          also have "… ≤ norm (X m - X n) * norm x"
             by (rule norm_blinfun)
          also have "… ≤ norm (X m - X n) * 1"
            using ‹norm x ≤ 1› norm_ge_zero by (rule mult_left_mono)
          also have "… = norm (X m - X n)" by simp
          also have "… < e" using le by fact
          finally show "norm (X m x - X n x) < e" .
        qed
      qed
      hence "convergent (λn. X n x)"
        by (metis Cauchy_convergent_iff)
    } note convergent_norm1 = this
    define y where "y = x /R norm x"
    have y: "norm y ≤ 1" and xy: "x = norm x *R y"
      by (simp_all add: y_def inverse_eq_divide)
    have "convergent (λn. norm x *R X n y)"
      by (intro bounded_bilinear.convergent[OF bounded_bilinear_scaleR] convergent_const
        convergent_norm1 y)
    also have "(λn. norm x *R X n y) = (λn. X n x)"
      by (subst xy) (simp add: blinfun.bilinear_simps)
    finally have "convergent (λn. X n x)" .
  }
  then obtain v where v: "⋀x. (λn. X n x) ⇢ v x"
    unfolding convergent_def
    by metis

  have "Cauchy (λn. norm (X n))"
  proof (rule CauchyI)
    fix e::real
    assume "e > 0"
    from CauchyD[OF ‹Cauchy X› ‹0 < e›] obtain M
      where M: "⋀m n. m ≥ M ⟹ n ≥ M ⟹ norm (X m - X n) < e"
      by auto
    show "∃M. ∀m≥M. ∀n≥M. norm (norm (X m) - norm (X n)) < e"
    proof (safe intro!: exI[where x=M])
      fix m n assume mn: "m ≥ M" "n ≥ M"
      have "norm (norm (X m) - norm (X n)) ≤ norm (X m - X n)"
        by (metis norm_triangle_ineq3 real_norm_def)
      also have "… < e" using mn by fact
      finally show "norm (norm (X m) - norm (X n)) < e" .
    qed
  qed
  then obtain K where K: "(λn. norm (X n)) ⇢ K"
    unfolding Cauchy_convergent_iff convergent_def
    by metis

  have "bounded_linear v"
  proof
    fix x y and r::real
    from tendsto_add[OF v[of x] v [of y]] v[of "x + y", unfolded blinfun.bilinear_simps]
      tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *R x", unfolded blinfun.bilinear_simps]
    show "v (x + y) = v x + v y" "v (r *R x) = r *R v x"
      by (metis (poly_guards_query) LIMSEQ_unique)+
    show "∃K. ∀x. norm (v x) ≤ norm x * K"
    proof (safe intro!: exI[where x=K])
      fix x
      have "norm (v x) ≤ K * norm x"
        by (rule tendsto_le[OF _ tendsto_mult[OF K tendsto_const] tendsto_norm[OF v]])
          (auto simp: norm_blinfun)
      thus "norm (v x) ≤ norm x * K"
        by (simp add: ac_simps)
    qed
  qed
  hence Bv: "⋀x. (λn. X n x) ⇢ Blinfun v x"
    by (auto simp: bounded_linear_Blinfun_apply v)

  have "X ⇢ Blinfun v"
  proof (rule LIMSEQ_I)
    fix r::real assume "r > 0"
    define r' where "r' = r / 2"
    have "0 < r'" "r' < r" using ‹r > 0› by (simp_all add: r'_def)
    from CauchyD[OF ‹Cauchy X› ‹r' > 0›]
    obtain M where M: "⋀m n. m ≥ M ⟹ n ≥ M ⟹ norm (X m - X n) < r'"
      by metis
    show "∃no. ∀n≥no. norm (X n - Blinfun v) < r"
    proof (safe intro!: exI[where x=M])
      fix n assume n: "M ≤ n"
      have "norm (X n - Blinfun v) ≤ r'"
      proof (rule norm_blinfun_bound)
        fix x
        have "eventually (λm. m ≥ M) sequentially"
          by (metis eventually_ge_at_top)
        hence ev_le: "eventually (λm. norm (X n x - X m x) ≤ r' * norm x) sequentially"
        proof eventually_elim
          case (elim m)
          have "norm (X n x - X m x) = norm ((X n - X m) x)"
            by (simp add: blinfun.bilinear_simps)
          also have "… ≤ norm ((X n - X m)) * norm x"
            by (rule norm_blinfun)
          also have "… ≤ r' * norm x"
            using M[OF n elim] by (simp add: mult_right_mono)
          finally show ?case .
        qed
        have tendsto_v: "(λm. norm (X n x - X m x)) ⇢ norm (X n x - Blinfun v x)"
          by (auto intro!: tendsto_intros Bv)
        show "norm ((X n - Blinfun v) x) ≤ r' * norm x"
          by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
      qed (simp add: ‹0 < r'› less_imp_le)
      thus "norm (X n - Blinfun v) < r"
        by (metis ‹r' < r› le_less_trans)
    qed
  qed
  thus "convergent X"
    by (rule convergentI)
qed

subsection ‹On Euclidean Space›

lemma Zfun_sum:
  assumes "finite s"
  assumes f: "⋀i. i ∈ s ⟹ Zfun (f i) F"
  shows "Zfun (λx. sum (λi. f i x) s) F"
  using assms by induct (auto intro!: Zfun_zero Zfun_add)

lemma norm_blinfun_euclidean_le:
  fixes a::"'a::euclidean_space ⇒L 'b::real_normed_vector"
  shows "norm a ≤ sum (λx. norm (a x)) Basis"
  apply (rule norm_blinfun_bound)
   apply (simp add: sum_nonneg)
  apply (subst euclidean_representation[symmetric, where 'a='a])
  apply (simp only: blinfun.bilinear_simps sum_distrib_right)
  apply (rule order.trans[OF norm_sum sum_mono])
  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
  done

lemma tendsto_componentwise1:
  fixes a::"'a::euclidean_space ⇒L 'b::real_normed_vector"
    and b::"'c ⇒ 'a ⇒L 'b"
  assumes "(⋀j. j ∈ Basis ⟹ ((λn. b n j) ⤏ a j) F)"
  shows "(b ⤏ a) F"
proof -
  have "⋀j. j ∈ Basis ⟹ Zfun (λx. norm (b x j - a j)) F"
    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
  hence "Zfun (λx. ∑j∈Basis. norm (b x j - a j)) F"
    by (auto intro!: Zfun_sum)
  thus ?thesis
    unfolding tendsto_Zfun_iff
    by (rule Zfun_le)
      (auto intro!: order_trans[OF norm_blinfun_euclidean_le] simp: blinfun.bilinear_simps)
qed

lift_definition
  blinfun_of_matrix::"('b::euclidean_space ⇒ 'a::euclidean_space ⇒ real) ⇒ 'a ⇒L 'b"
  is "λa x. ∑i∈Basis. ∑j∈Basis. ((x ∙ j) * a i j) *R i"
  by (intro bounded_linear_intros)

lemma blinfun_of_matrix_works:
  fixes f::"'a::euclidean_space ⇒L 'b::euclidean_space"
  shows "blinfun_of_matrix (λi j. (f j) ∙ i) = f"
proof (transfer, rule,  rule euclidean_eqI)
  fix f::"'a ⇒ 'b" and x::'a and b::'b assume "bounded_linear f" and b: "b ∈ Basis"
  then interpret bounded_linear f by simp
  have "(∑j∈Basis. ∑i∈Basis. (x ∙ i * (f i ∙ j)) *R j) ∙ b
    = (∑j∈Basis. if j = b then (∑i∈Basis. (x ∙ i * (f i ∙ j))) else 0)"
    using b
    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
  also have "… = (∑i∈Basis. (x ∙ i * (f i ∙ b)))"
    using b by (simp add: sum.delta)
  also have "… = f x ∙ b"
    by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms)
  finally show "(∑j∈Basis. ∑i∈Basis. (x ∙ i * (f i ∙ j)) *R j) ∙ b = f x ∙ b" .
qed

lemma blinfun_of_matrix_apply:
  "blinfun_of_matrix a x = (∑i∈Basis. ∑j∈Basis. ((x ∙ j) * a i j) *R i)"
  by transfer simp

lemma blinfun_of_matrix_minus: "blinfun_of_matrix x - blinfun_of_matrix y = blinfun_of_matrix (x - y)"
  by transfer (auto simp: algebra_simps sum_subtractf)

lemma norm_blinfun_of_matrix:
  "norm (blinfun_of_matrix a) ≤ (∑i∈Basis. ∑j∈Basis. ¦a i j¦)"
  apply (rule norm_blinfun_bound)
   apply (simp add: sum_nonneg)
  apply (simp only: blinfun_of_matrix_apply sum_distrib_right)
  apply (rule order_trans[OF norm_sum sum_mono])
  apply (rule order_trans[OF norm_sum sum_mono])
  apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
  done

lemma tendsto_blinfun_of_matrix:
  assumes "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ ((λn. b n i j) ⤏ a i j) F"
  shows "((λn. blinfun_of_matrix (b n)) ⤏ blinfun_of_matrix a) F"
proof -
  have "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ Zfun (λx. norm (b x i j - a i j)) F"
    using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
  hence "Zfun (λx. (∑i∈Basis. ∑j∈Basis. ¦b x i j - a i j¦)) F"
    by (auto intro!: Zfun_sum)
  thus ?thesis
    unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
    by (rule Zfun_le) (auto intro!: order_trans[OF norm_blinfun_of_matrix])
qed

lemma tendsto_componentwise:
  fixes a::"'a::euclidean_space ⇒L 'b::euclidean_space"
    and b::"'c ⇒ 'a ⇒L 'b"
  shows "(⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ ((λn. b n j ∙ i) ⤏ a j ∙ i) F) ⟹ (b ⤏ a) F"
  apply (subst blinfun_of_matrix_works[of a, symmetric])
  apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
  by (rule tendsto_blinfun_of_matrix)

lemma
  continuous_blinfun_componentwiseI:
  fixes f:: "'b::t2_space ⇒ 'a::euclidean_space ⇒L 'c::euclidean_space"
  assumes "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ continuous F (λx. (f x) j ∙ i)"
  shows "continuous F f"
  using assms by (auto simp: continuous_def intro!: tendsto_componentwise)

lemma
  continuous_blinfun_componentwiseI1:
  fixes f:: "'b::t2_space ⇒ 'a::euclidean_space ⇒L 'c::real_normed_vector"
  assumes "⋀i. i ∈ Basis ⟹ continuous F (λx. f x i)"
  shows "continuous F f"
  using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)

lemma
  continuous_on_blinfun_componentwise:
  fixes f:: "'d::t2_space ⇒ 'e::euclidean_space ⇒L 'f::real_normed_vector"
  assumes "⋀i. i ∈ Basis ⟹ continuous_on s (λx. f x i)"
  shows "continuous_on s f"
  using assms
  by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
    simp: continuous_on_eq_continuous_within continuous_def)

lemma bounded_linear_blinfun_matrix: "bounded_linear (λx. (x::_⇒L _) j ∙ i)"
  by (auto intro!: bounded_linearI' bounded_linear_intros)

lemma continuous_blinfun_matrix:
  fixes f:: "'b::t2_space ⇒ 'a::real_normed_vector ⇒L 'c::real_inner"
  assumes "continuous F f"
  shows "continuous F (λx. (f x) j ∙ i)"
  by (rule bounded_linear.continuous[OF bounded_linear_blinfun_matrix assms])

lemma continuous_on_blinfun_matrix:
  fixes f::"'a::t2_space ⇒ 'b::real_normed_vector ⇒L 'c::real_inner"
  assumes "continuous_on S f"
  shows "continuous_on S (λx. (f x) j ∙ i)"
  using assms
  by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)

lemma continuous_on_blinfun_of_matrix[continuous_intros]:
  assumes "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ continuous_on S (λs. g s i j)"
  shows "continuous_on S (λs. blinfun_of_matrix (g s))"
  using assms
  by (auto simp: continuous_on intro!: tendsto_blinfun_of_matrix)

lemma mult_if_delta:
  "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
  by auto

lemma compact_blinfun_lemma:
  fixes f :: "nat ⇒ 'a::euclidean_space ⇒L 'b::euclidean_space"
  assumes "bounded (range f)"
  shows "∀d⊆Basis. ∃l::'a ⇒L 'b. ∃ r::nat⇒nat.
    strict_mono r ∧ (∀e>0. eventually (λn. ∀i∈d. dist (f (r n) i) (l i) < e) sequentially)"
  by (rule compact_lemma_general[where unproj = "λe. blinfun_of_matrix (λi j. e j ∙ i)"])
   (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
    simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta sum.delta'
      scaleR_sum_left[symmetric])

lemma blinfun_euclidean_eqI: "(⋀i. i ∈ Basis ⟹ blinfun_apply x i = blinfun_apply y i) ⟹ x = y"
  apply (auto intro!: blinfun_eqI)
  apply (subst (2) euclidean_representation[symmetric, where 'a='a])
  apply (subst (1) euclidean_representation[symmetric, where 'a='a])
  apply (simp add: blinfun.bilinear_simps)
  done

lemma Blinfun_eq_matrix: "bounded_linear f ⟹ Blinfun f = blinfun_of_matrix (λi j. f j ∙ i)"
  by (intro blinfun_euclidean_eqI)
     (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
      if_distribR sum.delta' euclidean_representation
      cong: if_cong)

text ‹TODO: generalize (via ‹compact_cball›)?›
instance blinfun :: (euclidean_space, euclidean_space) heine_borel
proof
  fix f :: "nat ⇒ 'a ⇒L 'b"
  assume f: "bounded (range f)"
  then obtain l::"'a ⇒L 'b" and r where r: "strict_mono r"
    and l: "∀e>0. eventually (λn. ∀i∈Basis. dist (f (r n) i) (l i) < e) sequentially"
    using compact_blinfun_lemma [OF f] by blast
  {
    fix e::real
    let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
    assume "e > 0"
    hence "e / ?d > 0" by (simp add: DIM_positive)
    with l have "eventually (λn. ∀i∈Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
      by simp
    moreover
    {
      fix n
      assume n: "∀i∈Basis. dist (f (r n) i) (l i) < e / ?d"
      have "norm (f (r n) - l) = norm (blinfun_of_matrix (λi j. (f (r n) - l) j ∙ i))"
        unfolding blinfun_of_matrix_works ..
      also note norm_blinfun_of_matrix
      also have "(∑i∈Basis. ∑j∈Basis. ¦(f (r n) - l) j ∙ i¦) <
        (∑i∈(Basis::'b set). e / real_of_nat DIM('b))"
      proof (rule sum_strict_mono)
        fix i::'b assume i: "i ∈ Basis"
        have "(∑j::'a∈Basis. ¦(f (r n) - l) j ∙ i¦) < (∑j::'a∈Basis. e / ?d)"
        proof (rule sum_strict_mono)
          fix j::'a assume j: "j ∈ Basis"
          have "¦(f (r n) - l) j ∙ i¦ ≤ norm ((f (r n) - l) j)"
            by (simp add: Basis_le_norm i)
          also have "… < e / ?d"
            using n i j by (auto simp: dist_norm blinfun.bilinear_simps)
          finally show "¦(f (r n) - l) j ∙ i¦ < e / ?d" by simp
        qed simp_all
        also have "… ≤ e / real_of_nat DIM('b)"
          by simp
        finally show "(∑j∈Basis. ¦(f (r n) - l) j ∙ i¦) < e / real_of_nat DIM('b)"
          by simp
      qed simp_all
      also have "… ≤ e" by simp
      finally have "dist (f (r n)) l < e"
        by (auto simp: dist_norm)
    }
    ultimately have "eventually (λn. dist (f (r n)) l < e) sequentially"
      using eventually_elim2 by force
  }
  then have *: "((f ∘ r) ⤏ l) sequentially"
    unfolding o_def tendsto_iff by simp
  with r show "∃l r. strict_mono r ∧ ((f ∘ r) ⤏ l) sequentially"
    by auto
qed


subsection ‹concrete bounded linear functions›

lemma transfer_bounded_bilinear_bounded_linearI:
  assumes "g = (λi x. (blinfun_apply (f i) x))"
  shows "bounded_bilinear g = bounded_linear f"
proof
  assume "bounded_bilinear g"
  then interpret bounded_bilinear f by (simp add: assms)
  show "bounded_linear f"
  proof (unfold_locales, safe intro!: blinfun_eqI)
    fix i
    show "f (x + y) i = (f x + f y) i" "f (r *R x) i = (r *R f x) i" for r x y
      by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
    from _ nonneg_bounded show "∃K. ∀x. norm (f x) ≤ norm x * K"
      by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq ac_simps)
  qed
qed (auto simp: assms intro!: blinfun.comp)

lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
  "(rel_fun (rel_fun (=) (pcr_blinfun (=) (=))) (=)) bounded_bilinear bounded_linear"
  by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
    intro!: transfer_bounded_bilinear_bounded_linearI)

context bounded_bilinear
begin

lift_definition prod_left::"'b ⇒ 'a ⇒L 'c" is "(λb a. prod a b)"
  by (rule bounded_linear_left)
declare prod_left.rep_eq[simp]

lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
  by transfer (rule flip)

lift_definition prod_right::"'a ⇒ 'b ⇒L 'c" is "(λa b. prod a b)"
  by (rule bounded_linear_right)
declare prod_right.rep_eq[simp]

lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
  by transfer (rule bounded_bilinear_axioms)

end

lift_definition id_blinfun::"'a::real_normed_vector ⇒L 'a" is "λx. x"
  by (rule bounded_linear_ident)

lemmas blinfun_apply_id_blinfun[simp] = id_blinfun.rep_eq

lemma norm_blinfun_id[simp]:
  "norm (id_blinfun::'a::{real_normed_vector, perfect_space} ⇒L 'a) = 1"
  by transfer (auto simp: onorm_id)

lemma norm_blinfun_id_le:
  "norm (id_blinfun::'a::real_normed_vector ⇒L 'a) ≤ 1"
  by transfer (auto simp: onorm_id_le)


lift_definition fst_blinfun::"('a::real_normed_vector × 'b::real_normed_vector) ⇒L 'a" is fst
  by (rule bounded_linear_fst)

lemma blinfun_apply_fst_blinfun[simp]: "blinfun_apply fst_blinfun = fst"
  by transfer (rule refl)


lift_definition snd_blinfun::"('a::real_normed_vector × 'b::real_normed_vector) ⇒L 'b" is snd
  by (rule bounded_linear_snd)

lemma blinfun_apply_snd_blinfun[simp]: "blinfun_apply snd_blinfun = snd"
  by transfer (rule refl)


lift_definition blinfun_compose::
  "'a::real_normed_vector ⇒L 'b::real_normed_vector ⇒
    'c::real_normed_vector ⇒L 'a ⇒
    'c ⇒L 'b" (infixl "oL" 55) is "(o)"
  parametric comp_transfer
  unfolding o_def
  by (rule bounded_linear_compose)

lemma blinfun_apply_blinfun_compose[simp]: "(a oL b) c = a (b c)"
  by (simp add: blinfun_compose.rep_eq)

lemma norm_blinfun_compose:
  "norm (f oL g) ≤ norm f * norm g"
  by transfer (rule onorm_compose)

lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear (oL)"
  by unfold_locales
    (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)

lemma blinfun_compose_zero[simp]:
  "blinfun_compose 0 = (λ_. 0)"
  "blinfun_compose x 0 = 0"
  by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)


lift_definition blinfun_inner_right::"'a::real_inner ⇒ 'a ⇒L real" is "(∙)"
  by (rule bounded_linear_inner_right)
declare blinfun_inner_right.rep_eq[simp]

lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
  by transfer (rule bounded_bilinear_inner)


lift_definition blinfun_inner_left::"'a::real_inner ⇒ 'a ⇒L real" is "λx y. y ∙ x"
  by (rule bounded_linear_inner_left)
declare blinfun_inner_left.rep_eq[simp]

lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])


lift_definition blinfun_scaleR_right::"real ⇒ 'a ⇒L 'a::real_normed_vector" is "( *R)"
  by (rule bounded_linear_scaleR_right)
declare blinfun_scaleR_right.rep_eq[simp]

lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
  by transfer (rule bounded_bilinear_scaleR)


lift_definition blinfun_scaleR_left::"'a::real_normed_vector ⇒ real ⇒L 'a" is "λx y. y *R x"
  by (rule bounded_linear_scaleR_left)
lemmas [simp] = blinfun_scaleR_left.rep_eq

lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])


lift_definition blinfun_mult_right::"'a ⇒ 'a ⇒L 'a::real_normed_algebra" is "( * )"
  by (rule bounded_linear_mult_right)
declare blinfun_mult_right.rep_eq[simp]

lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
  by transfer (rule bounded_bilinear_mult)


lift_definition blinfun_mult_left::"'a::real_normed_algebra ⇒ 'a ⇒L 'a" is "λx y. y * x"
  by (rule bounded_linear_mult_left)
lemmas [simp] = blinfun_mult_left.rep_eq

lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
  by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])

lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
  bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
  bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
  bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]

end