--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 29 12:58:55 2016 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 28 16:15:51 2016 +0200
@@ -16,6 +16,28 @@
subsection \<open>Sundries\<close>
+
+text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
+lemma wf_finite_segments:
+ assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
+ shows "wf (r)"
+ apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
+ using acyclic_def assms irrefl_def trans_Restr by fastforce
+
+text\<open>For creating values between @{term u} and @{term v}.\<close>
+lemma scaling_mono:
+ fixes u::"'a::linordered_field"
+ assumes "u \<le> v" "0 \<le> r" "r \<le> s"
+ shows "u + r * (v - u) / s \<le> v"
+proof -
+ have "r/s \<le> 1" using assms
+ using divide_le_eq_1 by fastforce
+ then have "(r/s) * (v - u) \<le> 1 * (v - u)"
+ by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
+ then show ?thesis
+ by (simp add: field_simps)
+qed
+
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
@@ -4767,7 +4789,7 @@
qed
lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
- using negligible_Un negligible_subset by blast
+ using negligible_Un negligible_subset by blast
lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
@@ -10709,6 +10731,277 @@
(insert assms, simp_all add: powr_minus powr_realpow divide_simps)
qed
+subsubsection \<open>Covering lemma\<close>
+
+
+text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
+ lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
+ "Introduction to Gauge Integrals". \<close>
+
+proposition covering_lemma:
+ assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
+ obtains \<D> where
+ "countable \<D>" "\<Union>\<D> \<subseteq> cbox a b"
+ "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+ "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
+ "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
+ "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ "S \<subseteq> \<Union>\<D>"
+proof -
+ have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
+ using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
+ let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
+ cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
+ (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
+ let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
+ obtain \<D>0 where count: "countable \<D>0"
+ and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
+ and int: "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+ and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+ and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
+ and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
+ proof
+ show "countable ?D0"
+ by (simp add: countable_PiE)
+ next
+ show "\<Union>?D0 \<subseteq> cbox a b"
+ apply (simp add: UN_subset_iff)
+ apply (intro conjI allI ballI subset_box_imp)
+ apply (simp add: divide_simps zero_le_mult_iff aibi)
+ apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
+ done
+ next
+ show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+ using \<open>box a b \<noteq> {}\<close>
+ by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
+ next
+ have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
+ using of_nat_less_iff less_imp_of_nat_less by fastforce
+ have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+ for m n --\<open>The symmetry argument requires a single HOL formula\<close>
+ proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
+ fix v w m and n::nat
+ assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
+ have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+ apply (simp add: subset_box disjoint_interval)
+ apply (rule ccontr)
+ apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
+ apply (drule_tac x=i in bspec, assumption)
+ using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
+ apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
+ apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
+ done
+ then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+ by meson
+ qed auto
+ show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+ apply (erule imageE SigmaE)+
+ using * by simp
+ next
+ show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
+ proof (simp only: bex_simps split_paired_Bex_Sigma)
+ show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
+ proof -
+ obtain e where "0 < e"
+ and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
+ proof -
+ have "x \<in> g x" "open (g x)"
+ using \<open>gauge g\<close> by (auto simp: gauge_def)
+ then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
+ using openE by blast
+ have "norm (x - y) < \<epsilon>"
+ if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
+ proof -
+ have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
+ by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
+ also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
+ by (meson setsum_bounded_above that)
+ also have "... = \<epsilon> / 2"
+ by (simp add: divide_simps)
+ also have "... < \<epsilon>"
+ by (simp add: \<open>0 < \<epsilon>\<close>)
+ finally show ?thesis .
+ qed
+ then show ?thesis
+ by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add: \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
+ qed
+ have xab: "x \<in> cbox a b"
+ using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
+ obtain n where n: "norm (b - a) / 2^n < e"
+ using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
+ by (auto simp: divide_simps)
+ then have "norm (b - a) < e * 2^n"
+ by (auto simp: divide_simps)
+ then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
+ proof -
+ have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
+ by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
+ also have "... < e * 2 ^ n"
+ using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
+ finally show ?thesis .
+ qed
+ have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
+ for a m n x and y::real
+ by auto
+ have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
+ x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
+ proof
+ fix i::'a assume "i \<in> Basis"
+ consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
+ using \<open>i \<in> Basis\<close> mem_box(2) xab by force
+ then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
+ x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
+ proof cases
+ case 1 then show ?thesis
+ by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
+ next
+ case 2
+ then have abi_less: "a \<bullet> i < b \<bullet> i"
+ using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
+ let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
+ show ?thesis
+ proof (intro exI conjI)
+ show "?k < 2 ^ n"
+ using aibi xab \<open>i \<in> Basis\<close>
+ by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
+ next
+ have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
+ a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+ apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
+ using aibi [OF \<open>i \<in> Basis\<close>] xab 2
+ apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
+ done
+ also have "... = x \<bullet> i"
+ using abi_less by (simp add: divide_simps)
+ finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
+ next
+ have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+ using abi_less by (simp add: divide_simps algebra_simps)
+ also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+ apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
+ using aibi [OF \<open>i \<in> Basis\<close>] xab
+ apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
+ done
+ finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
+ qed
+ qed
+ qed
+ then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
+ apply (simp add: mem_box Bex_def)
+ apply (clarify dest!: bchoice)
+ apply (rule_tac x="restrict f Basis" in exI, simp)
+ done
+ moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
+ apply (clarsimp simp add: mem_box)
+ apply (rule e)
+ apply (drule bspec D, assumption)+
+ apply (erule order_trans)
+ apply (simp add: divide_simps)
+ using bai by (force simp: algebra_simps)
+ ultimately show ?thesis by auto
+ qed
+ qed
+ next
+ show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
+ next
+ obtain j::'a where "j \<in> Basis"
+ using nonempty_Basis by blast
+ have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
+ proof (rule finite_subset)
+ let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
+ (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
+ ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
+ have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
+ proof -
+ have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
+ \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
+ by (auto simp: divide_simps algebra_simps)
+ have bjaj: "b \<bullet> j - a \<bullet> j > 0"
+ using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
+ have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
+ (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
+ using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
+ then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
+ ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
+ by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
+ then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
+ by (rule dd)
+ then have "m \<le> n"
+ by auto
+ show ?thesis
+ by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
+ qed
+ then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
+ by auto
+ show "finite ?B"
+ by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
+ qed
+ then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
+ using that by auto
+ qed
+ let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
+ obtain \<D> where count: "countable \<D>"
+ and sub: "\<Union>\<D> \<subseteq> cbox a b" "S \<subseteq> \<Union>\<D>"
+ and int: "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+ and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+ and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
+ and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
+ proof
+ show "countable ?D1" using count countable_subset
+ by (simp add: count countable_subset)
+ show "\<Union>?D1 \<subseteq> cbox a b"
+ using sub by blast
+ show "S \<subseteq> \<Union>?D1"
+ using SK by (force simp:)
+ show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+ using int by blast
+ show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+ using intdj by blast
+ show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
+ by auto
+ show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ using cbox by blast
+ show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
+ using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
+ qed
+ let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
+ show ?thesis
+ proof (rule that)
+ show "countable ?\<D>"
+ by (blast intro: countable_subset [OF _ count])
+ show "\<Union>?\<D> \<subseteq> cbox a b"
+ using sub by blast
+ show "S \<subseteq> \<Union>?\<D>"
+ proof clarsimp
+ fix x
+ assume "x \<in> S"
+ then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
+ let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
+ have irrR: "irrefl ?R" by (force simp: irrefl_def)
+ have traR: "trans ?R" by (force simp: trans_def)
+ have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
+ by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
+ have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
+ using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
+ then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
+ by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
+ then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
+ by blast
+ qed
+ show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+ by (blast intro: dest: int)
+ show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
+ using intdj by (simp add: pairwise_def) metis
+ show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
+ using SK by force
+ show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+ using cbox by force
+ qed
+qed
+
subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
lemma integral_component_eq_cart[simp]: