src/HOL/Probability/Bochner_Integration.thy
changeset 57036 22568fb89165
parent 57025 e7fd64f82876
child 57137 f174712d0a84
     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Wed May 21 12:49:27 2014 +0200
     1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Wed May 21 13:52:46 2014 +0200
     1.3 @@ -563,7 +563,7 @@
     1.4      by (metis has_bochner_integral_simple_bochner_integrable)
     1.5  qed
     1.6  
     1.7 -lemma has_bochner_integral_add:
     1.8 +lemma has_bochner_integral_add[intro]:
     1.9    "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
    1.10      has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
    1.11  proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
    1.12 @@ -713,8 +713,7 @@
    1.13  lemma has_bochner_integral_setsum:
    1.14    "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
    1.15      has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
    1.16 -  by (induct I rule: infinite_finite_induct)
    1.17 -     (auto intro: has_bochner_integral_zero has_bochner_integral_add)
    1.18 +  by (induct I rule: infinite_finite_induct) auto
    1.19  
    1.20  lemma has_bochner_integral_implies_finite_norm:
    1.21    "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
    1.22 @@ -918,7 +917,7 @@
    1.23    by (intro has_bochner_integral_cong_AE arg_cong[where f=The] ext)
    1.24  
    1.25  lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
    1.26 -  by (auto simp: integrable.simps intro: has_bochner_integral_add)
    1.27 +  by (auto simp: integrable.simps)
    1.28  
    1.29  lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
    1.30    by (metis has_bochner_integral_zero integrable.simps) 
    1.31 @@ -1383,6 +1382,56 @@
    1.32    finally show ?thesis .
    1.33  qed
    1.34  
    1.35 +lemma
    1.36 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
    1.37 +  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
    1.38 +  and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
    1.39 +  and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
    1.40 +  shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
    1.41 +    and sums_integral: "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is "?f sums ?x")
    1.42 +    and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
    1.43 +    and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
    1.44 +proof -
    1.45 +  have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
    1.46 +  proof (rule integrableI_bounded)
    1.47 +    have "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) = (\<integral>\<^sup>+ x. (\<Sum>i. ereal (norm (f i x))) \<partial>M)"
    1.48 +      apply (intro nn_integral_cong_AE) 
    1.49 +      using summable
    1.50 +      apply eventually_elim
    1.51 +      apply (simp add: suminf_ereal' suminf_nonneg)
    1.52 +      done
    1.53 +    also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
    1.54 +      by (intro nn_integral_suminf) auto
    1.55 +    also have "\<dots> = (\<Sum>i. ereal (\<integral>x. norm (f i x) \<partial>M))"
    1.56 +      by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
    1.57 +    finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
    1.58 +      by (simp add: suminf_ereal' sums)
    1.59 +  qed simp
    1.60 +
    1.61 +  have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
    1.62 +    using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
    1.63 +
    1.64 +  have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
    1.65 +    using summable
    1.66 +  proof eventually_elim
    1.67 +    fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
    1.68 +    have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_setsum)
    1.69 +    also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
    1.70 +      using setsum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
    1.71 +    finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
    1.72 +  qed
    1.73 +
    1.74 +  note int = integral_dominated_convergence(1,3)[OF _ _ 1 2 3]
    1.75 +
    1.76 +  show "integrable M ?S"
    1.77 +    by (rule int) measurable
    1.78 +
    1.79 +  show "?f sums ?x" unfolding sums_def
    1.80 +    using int(2) by (simp add: integrable)
    1.81 +  then show "?x = suminf ?f" "summable ?f"
    1.82 +    unfolding sums_iff by auto
    1.83 +qed
    1.84 +
    1.85  lemma integral_norm_bound:
    1.86    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
    1.87    shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
    1.88 @@ -1475,8 +1524,7 @@
    1.89    shows "0 \<le> integral\<^sup>L M f"
    1.90  proof -
    1.91    have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
    1.92 -    by (subst integral_eq_nn_integral)
    1.93 -       (auto intro: real_of_ereal_pos nn_integral_nonneg integrable_max assms)
    1.94 +    by (subst integral_eq_nn_integral) (auto intro: real_of_ereal_pos nn_integral_nonneg assms)
    1.95    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
    1.96      using assms(2) by (intro integral_cong_AE assms integrable_max) auto
    1.97    finally show ?thesis
    1.98 @@ -1616,7 +1664,7 @@
    1.99        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
   1.100          unfolding lim(2)[symmetric]
   1.101          by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
   1.102 -           (insert lim(3-5), auto intro: integrable_norm)
   1.103 +           (insert lim(3-5), auto)
   1.104      qed
   1.105    qed
   1.106  qed (simp add: f g integrable_density)
   1.107 @@ -1686,7 +1734,7 @@
   1.108        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
   1.109        proof (rule integral_dominated_convergence(3))
   1.110          show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
   1.111 -          using lim by (auto intro!: integrable_norm simp: integrable_distr_eq) 
   1.112 +          using lim by (auto simp: integrable_distr_eq) 
   1.113          show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
   1.114            using lim(3) g[THEN measurable_space] by auto
   1.115          show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
   1.116 @@ -1695,7 +1743,7 @@
   1.117        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
   1.118          unfolding lim(2)[symmetric]
   1.119          by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
   1.120 -           (insert lim(3-5), auto intro: integrable_norm)
   1.121 +           (insert lim(3-5), auto)
   1.122      qed
   1.123    qed
   1.124  qed (simp add: f g integrable_distr_eq)
   1.125 @@ -1764,9 +1812,9 @@
   1.126    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
   1.127      by (intro integral_diff integrable_max integrable_minus integrable_zero f)
   1.128    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
   1.129 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   1.130 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
   1.131    also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
   1.132 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
   1.133 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
   1.134    also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
   1.135      by (auto simp: max_def)
   1.136    also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
   1.137 @@ -1967,73 +2015,10 @@
   1.138    shows "integral\<^sup>L M X < integral\<^sup>L M Y"
   1.139    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
   1.140  
   1.141 -(* GENERALIZE to banach, sct *)
   1.142 -lemma integral_sums:
   1.143 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   1.144 -  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
   1.145 -  and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
   1.146 -  and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
   1.147 -  shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
   1.148 -  and "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is ?integral)
   1.149 -proof -
   1.150 -  have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
   1.151 -    using summable unfolding summable_def by auto
   1.152 -  from bchoice[OF this]
   1.153 -  obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
   1.154 -  then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
   1.155 -    by (rule borel_measurable_LIMSEQ) auto
   1.156 -
   1.157 -  let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
   1.158 -
   1.159 -  obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
   1.160 -    using sums unfolding summable_def ..
   1.161 -
   1.162 -  have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i<n. f i x)"
   1.163 -    using integrable by auto
   1.164 -
   1.165 -  have 2: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> ?w x"
   1.166 -    using AE_space
   1.167 -  proof eventually_elim
   1.168 -    fix j x assume [simp]: "x \<in> space M"
   1.169 -    have "\<bar>\<Sum>i<j. f i x\<bar> \<le> (\<Sum>i<j. \<bar>f i x\<bar>)" by (rule setsum_abs)
   1.170 -    also have "\<dots> \<le> w x" using w[of x] setsum_le_suminf[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
   1.171 -    finally show "norm (\<Sum>i<j. f i x) \<le> ?w x" by simp
   1.172 -  qed
   1.173 -
   1.174 -  have 3: "integrable M ?w"
   1.175 -  proof (rule integrable_monotone_convergence(1))
   1.176 -    let ?F = "\<lambda>n y. (\<Sum>i<n. \<bar>f i y\<bar>)"
   1.177 -    let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
   1.178 -    have "\<And>n. integrable M (?F n)"
   1.179 -      using integrable by (auto intro!: integrable_abs)
   1.180 -    thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
   1.181 -    show "AE x in M. mono (\<lambda>n. ?w' n x)"
   1.182 -      by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
   1.183 -    show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
   1.184 -        using w by (simp_all add: tendsto_const sums_def)
   1.185 -    have *: "\<And>n. integral\<^sup>L M (?w' n) = (\<Sum>i< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
   1.186 -      using integrable by (simp add: integrable_abs cong: integral_cong)
   1.187 -    from abs_sum
   1.188 -    show "(\<lambda>i. integral\<^sup>L M (?w' i)) ----> x" unfolding * sums_def .
   1.189 -  qed (simp add: w_borel measurable_If_set)
   1.190 -
   1.191 -  from summable[THEN summable_rabs_cancel]
   1.192 -  have 4: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
   1.193 -    by (auto intro: summable_LIMSEQ)
   1.194 -
   1.195 -  note int = integral_dominated_convergence(1,3)[OF _ _ 3 4 2]
   1.196 -
   1.197 -  from int show "integrable M ?S" by simp
   1.198 -
   1.199 -  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF integrable]
   1.200 -    using int(2) by simp
   1.201 -qed
   1.202 -
   1.203  lemma integrable_mult_indicator:
   1.204    fixes f :: "'a \<Rightarrow> real"
   1.205    shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
   1.206 -  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"])
   1.207 -     (auto intro: integrable_abs split: split_indicator)
   1.208 +  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"]) (auto split: split_indicator)
   1.209  
   1.210  lemma tendsto_integral_at_top:
   1.211    fixes f :: "real \<Rightarrow> real"
   1.212 @@ -2069,15 +2054,14 @@
   1.213    let ?p = "integral\<^sup>L M (\<lambda>x. max 0 (f x))"
   1.214    let ?n = "integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
   1.215    have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
   1.216 -    by (auto intro!: nonneg integrable_max f)
   1.217 +    by (auto intro!: nonneg f)
   1.218    note tendsto_diff[OF this]
   1.219    also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
   1.220      by (subst integral_diff[symmetric])
   1.221 -       (auto intro!: integrable_mult_indicator integrable_max f integral_cong
   1.222 +       (auto intro!: integrable_mult_indicator f integral_cong
   1.223               simp: M split: split_max)
   1.224    also have "?p - ?n = integral\<^sup>L M f"
   1.225 -    by (subst integral_diff[symmetric])
   1.226 -       (auto intro!: integrable_max f integral_cong simp: M split: split_max)
   1.227 +    by (subst integral_diff[symmetric]) (auto intro!: f integral_cong simp: M split: split_max)
   1.228    finally show ?thesis .
   1.229  qed
   1.230  
   1.231 @@ -2112,67 +2096,6 @@
   1.232      by (auto simp: _has_bochner_integral_iff)
   1.233  qed
   1.234  
   1.235 -
   1.236 -subsection {* Lebesgue integration on countable spaces *}
   1.237 -
   1.238 -lemma integral_on_countable:
   1.239 -  fixes f :: "real \<Rightarrow> real"
   1.240 -  assumes f: "f \<in> borel_measurable M"
   1.241 -  and bij: "bij_betw enum S (f ` space M)"
   1.242 -  and enum_zero: "enum ` (-S) \<subseteq> {0}"
   1.243 -  and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> (emeasure M) (f -` {x} \<inter> space M) \<noteq> \<infinity>"
   1.244 -  and abs_summable: "summable (\<lambda>r. \<bar>enum r * real ((emeasure M) (f -` {enum r} \<inter> space M))\<bar>)"
   1.245 -  shows "integrable M f"
   1.246 -  and "(\<lambda>r. enum r * real ((emeasure M) (f -` {enum r} \<inter> space M))) sums integral\<^sup>L M f" (is ?sums)
   1.247 -proof -
   1.248 -  let ?A = "\<lambda>r. f -` {enum r} \<inter> space M"
   1.249 -  let ?F = "\<lambda>r x. enum r * indicator (?A r) x"
   1.250 -  have enum_eq: "\<And>r. enum r * real ((emeasure M) (?A r)) = integral\<^sup>L M (?F r)"
   1.251 -    using f fin by (simp add: measure_def cong: disj_cong)
   1.252 -
   1.253 -  { fix x assume "x \<in> space M"
   1.254 -    hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto
   1.255 -    then obtain i where "i\<in>S" "enum i = f x" by auto
   1.256 -    have F: "\<And>j. ?F j x = (if j = i then f x else 0)"
   1.257 -    proof cases
   1.258 -      fix j assume "j = i"
   1.259 -      thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def)
   1.260 -    next
   1.261 -      fix j assume "j \<noteq> i"
   1.262 -      show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero
   1.263 -        by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def)
   1.264 -    qed
   1.265 -    hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto
   1.266 -    have "(\<lambda>i. ?F i x) sums f x"
   1.267 -         "(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>"
   1.268 -      by (auto intro!: sums_single simp: F F_abs) }
   1.269 -  note F_sums_f = this(1) and F_abs_sums_f = this(2)
   1.270 -
   1.271 -  have int_f: "integral\<^sup>L M f = (\<integral>x. (\<Sum>r. ?F r x) \<partial>M)" "integrable M f = integrable M (\<lambda>x. \<Sum>r. ?F r x)"
   1.272 -    using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
   1.273 -
   1.274 -  { fix r
   1.275 -    have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x \<partial>M)"
   1.276 -      by (auto simp: indicator_def intro!: integral_cong)
   1.277 -    also have "\<dots> = \<bar>enum r\<bar> * real ((emeasure M) (?A r))"
   1.278 -      using f fin by (simp add: measure_def cong: disj_cong)
   1.279 -    finally have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = \<bar>enum r * real ((emeasure M) (?A r))\<bar>"
   1.280 -      using f by (subst (2) abs_mult_pos[symmetric]) (auto intro!: real_of_ereal_pos measurable_sets) }
   1.281 -  note int_abs_F = this
   1.282 -
   1.283 -  have 1: "\<And>i. integrable M (\<lambda>x. ?F i x)"
   1.284 -    using f fin by auto
   1.285 -
   1.286 -  have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)"
   1.287 -    using F_abs_sums_f unfolding sums_iff by auto
   1.288 -
   1.289 -  from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
   1.290 -  show ?sums unfolding enum_eq int_f by simp
   1.291 -
   1.292 -  from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
   1.293 -  show "integrable M f" unfolding int_f by simp
   1.294 -qed
   1.295 -
   1.296  subsection {* Product measure *}
   1.297  
   1.298  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
   1.299 @@ -2419,7 +2342,7 @@
   1.300      show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
   1.301      proof (rule integral_dominated_convergence)
   1.302        show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
   1.303 -        using lim(5) by (auto intro: integrable_norm)
   1.304 +        using lim(5) by auto
   1.305      qed (insert lim, auto)
   1.306      have "(\<lambda>i. \<integral> x. \<integral> y. s i (x, y) \<partial>M2 \<partial>M1) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
   1.307      proof (rule integral_dominated_convergence)
   1.308 @@ -2433,7 +2356,7 @@
   1.309          show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
   1.310          proof (rule integral_dominated_convergence)
   1.311            show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
   1.312 -             using f by (auto intro: integrable_norm)
   1.313 +             using f by auto
   1.314            show "AE xa in M2. (\<lambda>i. s i (x, xa)) ----> f (x, xa)"
   1.315              using x lim(3) by (auto simp: space_pair_measure)
   1.316            show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"