equal
deleted
inserted
replaced
674 |
674 |
675 lemmas has_bochner_integral_divide = |
675 lemmas has_bochner_integral_divide = |
676 has_bochner_integral_bounded_linear[OF bounded_linear_divide] |
676 has_bochner_integral_bounded_linear[OF bounded_linear_divide] |
677 |
677 |
678 lemma has_bochner_integral_divide_zero[intro]: |
678 lemma has_bochner_integral_divide_zero[intro]: |
679 fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" |
679 fixes c :: "_::{real_normed_field, field, second_countable_topology}" |
680 shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)" |
680 shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)" |
681 using has_bochner_integral_divide by (cases "c = 0") auto |
681 using has_bochner_integral_divide by (cases "c = 0") auto |
682 |
682 |
683 lemma has_bochner_integral_inner_left[intro]: |
683 lemma has_bochner_integral_inner_left[intro]: |
684 "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)" |
684 "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)" |
988 fixes c :: "_::{real_normed_algebra,second_countable_topology}" |
988 fixes c :: "_::{real_normed_algebra,second_countable_topology}" |
989 shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)" |
989 shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)" |
990 unfolding integrable.simps by fastforce |
990 unfolding integrable.simps by fastforce |
991 |
991 |
992 lemma integrable_divide_zero[simp, intro]: |
992 lemma integrable_divide_zero[simp, intro]: |
993 fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" |
993 fixes c :: "_::{real_normed_field, field, second_countable_topology}" |
994 shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)" |
994 shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)" |
995 unfolding integrable.simps by fastforce |
995 unfolding integrable.simps by fastforce |
996 |
996 |
997 lemma integrable_inner_left[simp, intro]: |
997 lemma integrable_inner_left[simp, intro]: |
998 "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)" |
998 "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)" |
1096 |
1096 |
1097 lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f" |
1097 lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f" |
1098 by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right) |
1098 by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right) |
1099 |
1099 |
1100 lemma integral_divide_zero[simp]: |
1100 lemma integral_divide_zero[simp]: |
1101 fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" |
1101 fixes c :: "_::{real_normed_field, field, second_countable_topology}" |
1102 shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c" |
1102 shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c" |
1103 by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp |
1103 by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp |
1104 |
1104 |
1105 lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f" |
1105 lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f" |
1106 by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp |
1106 by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp |