equal
deleted
inserted
replaced
57 by (simp add: sum_strict_mono power_strict_mono assms) |
57 by (simp add: sum_strict_mono power_strict_mono assms) |
58 |
58 |
59 lemma L2_set_right_distrib: |
59 lemma L2_set_right_distrib: |
60 "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A" |
60 "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A" |
61 unfolding L2_set_def |
61 unfolding L2_set_def |
62 apply (simp add: power_mult_distrib) |
62 by (simp add: power_mult_distrib real_sqrt_mult sum_nonneg flip: sum_distrib_left) |
63 apply (simp add: sum_distrib_left [symmetric]) |
|
64 apply (simp add: real_sqrt_mult sum_nonneg) |
|
65 done |
|
66 |
63 |
67 lemma L2_set_left_distrib: |
64 lemma L2_set_left_distrib: |
68 "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A" |
65 "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A" |
69 unfolding L2_set_def power_mult_distrib |
66 unfolding L2_set_def power_mult_distrib |
70 by (simp add: real_sqrt_mult sum_nonneg flip: sum_distrib_right) |
67 by (simp add: real_sqrt_mult sum_nonneg flip: sum_distrib_right) |