# HG changeset patch # User paulson # Date 1523887246 -3600 # Node ID 706f86afff43106d60ff94576b9b55aa7ddc3c15 # Parent 01c6514120811178aa6e307768cbfd4a1ca1e3e7 more results about measure and negligibility diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Apr 16 05:34:25 2018 +0000 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Apr 16 15:00:46 2018 +0100 @@ -1116,6 +1116,36 @@ by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def) qed +lemma has_measure_limit: + assumes "S \ lmeasurable" "e > 0" + obtains B where "B > 0" + "\a b. ball 0 B \ cbox a b \ \measure lebesgue (S \ cbox a b) - measure lebesgue S\ < e" + using assms unfolding lmeasurable_iff_has_integral has_integral_alt' + by (force simp: integral_indicator integrable_on_indicator) + +lemma lmeasurable_iff_indicator_has_integral: + fixes S :: "'a::euclidean_space set" + shows "S \ lmeasurable \ m = measure lebesgue S \ (indicat_real S has_integral m) UNIV" + by (metis has_integral_iff lmeasurable_iff_has_integral measurable_integrable) + +lemma has_measure_limit_iff: + fixes f :: "'n::euclidean_space \ 'a::banach" + shows "S \ lmeasurable \ m = measure lebesgue S \ + (\e>0. \B>0. \a b. ball 0 B \ cbox a b \ + (S \ cbox a b) \ lmeasurable \ \measure lebesgue (S \ cbox a b) - m\ < e)" (is "?lhs = ?rhs") +proof + assume ?lhs then show ?rhs + by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox) +next + assume RHS [rule_format]: ?rhs + show ?lhs + apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m]) + using RHS + by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator) +qed + +subsection\Applications to Negligibility\ + lemma negligible_iff_null_sets: "negligible S \ S \ null_sets lebesgue" proof assume "negligible S" @@ -1172,8 +1202,6 @@ qed qed -subsection\Applications to Negligibility\ - lemma negligible_hyperplane: assumes "a \ 0 \ b \ 0" shows "negligible {x. a \ x = b}" proof - @@ -1258,7 +1286,6 @@ using frontier_cball negligible_convex_frontier convex_cball by (blast intro: negligible_subset) - lemma non_negligible_UNIV [simp]: "\ negligible UNIV" unfolding negligible_iff_null_sets by (auto simp: null_sets_def emeasure_lborel_UNIV) @@ -1268,6 +1295,36 @@ not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq intro: eq_refl antisym less_imp_le) +proposition open_not_negligible: + assumes "open S" "S \ {}" + shows "\ negligible S" +proof + assume neg: "negligible S" + obtain a where "a \ S" + using \S \ {}\ by blast + then obtain e where "e > 0" "cball a e \ S" + using \open S\ open_contains_cball_eq by blast + let ?p = "a - (e / DIM('a)) *\<^sub>R One" let ?q = "a + (e / DIM('a)) *\<^sub>R One" + have "cbox ?p ?q \ cball a e" + proof (clarsimp simp: mem_box dist_norm) + fix x + assume "\i\Basis. ?p \ i \ x \ i \ x \ i \ ?q \ i" + then have ax: "\(a - x) \ i\ \ e / real DIM('a)" if "i \ Basis" for i + using that by (auto simp: algebra_simps) + have "norm (a - x) \ (\i\Basis. \(a - x) \ i\)" + by (rule norm_le_l1) + also have "\ \ DIM('a) * (e / real DIM('a))" + by (intro sum_bounded_above ax) + also have "\ = e" + by simp + finally show "norm (a - x) \ e" . + qed + then have "negligible (cbox ?p ?q)" + by (meson \cball a e \ S\ neg negligible_subset) + with \e > 0\ show False + by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff) +qed + lemma measure_eq_0_null_sets: "S \ null_sets M \ measure M S = 0" by (auto simp: measure_def null_sets_def) @@ -1337,7 +1394,36 @@ by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0) qed -text\Negligibility of image under non-injective linear map\ +lemma measure_closure: + assumes "bounded S" and neg: "negligible (frontier S)" + shows "measure lebesgue (closure S) = measure lebesgue S" +proof - + have "measure lebesgue (frontier S) = 0" + by (metis neg negligible_imp_measure0) + then show ?thesis + by (metis assms lmeasurable_iff_integrable_on eq_iff_diff_eq_0 has_integral_interior integrable_on_def integral_unique lmeasurable_interior lmeasure_integral measure_frontier) +qed + +lemma measure_interior: + "\bounded S; negligible(frontier S)\ \ measure lebesgue (interior S) = measure lebesgue S" + using measure_closure measure_frontier negligible_imp_measure0 by fastforce + +lemma measurable_Jordan: + assumes "bounded S" and neg: "negligible (frontier S)" + shows "S \ lmeasurable" +proof - + have "closure S \ lmeasurable" + by (metis lmeasurable_closure \bounded S\) + moreover have "interior S \ lmeasurable" + by (simp add: lmeasurable_interior \bounded S\) + moreover have "interior S \ S" + by (simp add: interior_subset) + ultimately show ?thesis + using assms by (metis (full_types) closure_subset completion.complete_sets_sandwich_fmeasurable measure_closure measure_interior) +qed + +subsection\Negligibility of image under non-injective linear map\ + lemma negligible_Union_nat: assumes "\n::nat. negligible(S n)" shows "negligible(\n. S n)" @@ -1362,6 +1448,59 @@ using * by (simp add: negligible_UNIV has_integral_iff) qed + +lemma negligible_linear_singular_image: + fixes f :: "'n::euclidean_space \ 'n" + assumes "linear f" "\ inj f" + shows "negligible (f ` S)" +proof - + obtain a where "a \ 0" "\S. f ` S \ {x. a \ x = 0}" + using assms linear_singular_image_hyperplane by blast + then show "negligible (f ` S)" + by (metis negligible_hyperplane negligible_subset) +qed + +lemma measure_negligible_finite_Union: + assumes "finite \" + and meas: "\S. S \ \ \ S \ lmeasurable" + and djointish: "pairwise (\S T. negligible (S \ T)) \" + shows "measure lebesgue (\\) = (\S\\. measure lebesgue S)" + using assms +proof (induction) + case empty + then show ?case + by auto +next + case (insert S \) + then have "S \ lmeasurable" "\\ \ lmeasurable" "pairwise (\S T. negligible (S \ T)) \" + by (simp_all add: fmeasurable.finite_Union insert.hyps(1) insert.prems(1) pairwise_insert subsetI) + then show ?case + proof (simp add: measure_Un3 insert) + have *: "\T. T \ (\) S ` \ \ negligible T" + using insert by (force simp: pairwise_def) + have "negligible(S \ \\)" + unfolding Int_Union + by (rule negligible_Union) (simp_all add: * insert.hyps(1)) + then show "measure lebesgue (S \ \\) = 0" + using negligible_imp_measure0 by blast + qed +qed + +lemma measure_negligible_finite_Union_image: + assumes "finite S" + and meas: "\x. x \ S \ f x \ lmeasurable" + and djointish: "pairwise (\x y. negligible (f x \ f y)) S" + shows "measure lebesgue (\(f ` S)) = (\x\S. measure lebesgue (f x))" +proof - + have "measure lebesgue (\(f ` S)) = sum (measure lebesgue) (f ` S)" + using assms by (auto simp: pairwise_mono pairwise_image intro: measure_negligible_finite_Union) + also have "\ = sum (measure lebesgue \ f) S" + using djointish [unfolded pairwise_def] by (metis inf.idem negligible_imp_measure0 sum.reindex_nontrivial [OF \finite S\]) + also have "\ = (\x\S. measure lebesgue (f x))" + by simp + finally show ?thesis . +qed + subsection \Negligibility of a Lipschitz image of a negligible set\ text\The bound will be eliminated by a sort of onion argument\ @@ -1596,12 +1735,10 @@ by (auto simp: fbx_def) have 2: "I' \ \ \ finite I' \ measure lebesgue (\D\I'. fbx D) \ e/2" for I' by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def) - have 3: "0 \ e/2" - using \0 by auto show "(\D\\. fbx D) \ lmeasurable" - by (intro fmeasurable_UN_bound[OF \countable \\ 1 2 3]) + by (intro fmeasurable_UN_bound[OF \countable \\ 1 2]) have "measure lebesgue (\D\\. fbx D) \ e/2" - by (intro measure_UN_bound[OF \countable \\ 1 2 3]) + by (intro measure_UN_bound[OF \countable \\ 1 2]) then show "measure lebesgue (\D\\. fbx D) < e" using \0 < e\ by linarith qed @@ -1722,6 +1859,134 @@ done qed +subsection\Measurability of countable unions and intersections of various kinds.\ + +lemma + assumes S: "\n. S n \ lmeasurable" + and leB: "\n. measure lebesgue (S n) \ B" + and nest: "\n. S n \ S(Suc n)" + shows measurable_nested_Union: "(\n. S n) \ lmeasurable" + and measure_nested_Union: "(\n. measure lebesgue (S n)) \ measure lebesgue (\n. S n)" (is ?Lim) +proof - + have 1: "\n. (indicat_real (S n)) integrable_on UNIV" + using S measurable_integrable by blast + have 2: "\n x::'a. indicat_real (S n) x \ (indicat_real (S (Suc n)) x)" + by (simp add: indicator_leI nest rev_subsetD) + have 3: "\x. (\n. indicat_real (S n) x) \ (indicat_real (UNION UNIV S) x)" + apply (rule Lim_eventually) + apply (simp add: indicator_def) + by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE) + have 4: "bounded (range (\n. integral UNIV (indicat_real (S n))))" + using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff) + have "(\n. S n) \ lmeasurable \ ?Lim" + apply (simp add: lmeasure_integral_UNIV S cong: conj_cong) + apply (simp add: measurable_integrable) + apply (rule monotone_convergence_increasing [OF 1 2 3 4]) + done + then show "(\n. S n) \ lmeasurable" "?Lim" + by auto +qed + +lemma + assumes S: "\n. S n \ lmeasurable" + and djointish: "pairwise (\m n. negligible (S m \ S n)) UNIV" + and leB: "\n. (\k\n. measure lebesgue (S k)) \ B" + shows measurable_countable_negligible_Union: "(\n. S n) \ lmeasurable" + and measure_countable_negligible_Union: "(\n. (measure lebesgue (S n))) sums measure lebesgue (\n. S n)" (is ?Sums) +proof - + have 1: "UNION {..n} S \ lmeasurable" for n + using S by blast + have 2: "measure lebesgue (UNION {..n} S) \ B" for n + proof - + have "measure lebesgue (UNION {..n} S) \ (\k\n. measure lebesgue (S k))" + by (simp add: S fmeasurableD measure_UNION_le) + with leB show ?thesis + using order_trans by blast + qed + have 3: "\n. UNION {..n} S \ UNION {..Suc n} S" + by (simp add: SUP_subset_mono) + have eqS: "(\n. S n) = (\n. UNION {..n} S)" + using atLeastAtMost_iff by blast + also have "(\n. UNION {..n} S) \ lmeasurable" + by (intro measurable_nested_Union [OF 1 2] 3) + finally show "(\n. S n) \ lmeasurable" . + have eqm: "(\i\n. measure lebesgue (S i)) = measure lebesgue (UNION {..n} S)" for n + using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono) + have "(\n. (measure lebesgue (S n))) sums measure lebesgue (\n. UNION {..n} S)" + by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3) + then show ?Sums + by (simp add: eqS) +qed + +lemma negligible_countable_Union [intro]: + assumes "countable \" and meas: "\S. S \ \ \ negligible S" + shows "negligible (\\)" +proof (cases "\ = {}") + case False + then show ?thesis + by (metis from_nat_into range_from_nat_into assms negligible_Union_nat) +qed simp + +lemma + assumes S: "\n. (S n) \ lmeasurable" + and djointish: "pairwise (\m n. negligible (S m \ S n)) UNIV" + and bo: "bounded (\n. S n)" + shows measurable_countable_negligible_Union_bounded: "(\n. S n) \ lmeasurable" + and measure_countable_negligible_Union_bounded: "(\n. (measure lebesgue (S n))) sums measure lebesgue (\n. S n)" (is ?Sums) +proof - + obtain a b where ab: "(\n. S n) \ cbox a b" + using bo bounded_subset_cbox by blast + then have B: "(\k\n. measure lebesgue (S k)) \ measure lebesgue (cbox a b)" for n + proof - + have "(\k\n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)" + using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish + by (metis S finite_atMost subset_UNIV) + also have "\ \ measure lebesgue (cbox a b)" + apply (rule measure_mono_fmeasurable) + using ab S by force+ + finally show ?thesis . + qed + show "(\n. S n) \ lmeasurable" + by (rule measurable_countable_negligible_Union [OF S djointish B]) + show ?Sums + by (rule measure_countable_negligible_Union [OF S djointish B]) +qed + +lemma measure_countable_Union_approachable: + assumes "countable \" "e > 0" and measD: "\d. d \ \ \ d \ lmeasurable" + and B: "\D'. \D' \ \; finite D'\ \ measure lebesgue (\D') \ B" + obtains D' where "D' \ \" "finite D'" "measure lebesgue (\\) - e < measure lebesgue (\D')" +proof (cases "\ = {}") + case True + then show ?thesis + by (simp add: \e > 0\ that) +next + case False + let ?S = "\n. \k \ n. from_nat_into \ k" + have "(\n. measure lebesgue (?S n)) \ measure lebesgue (\n. ?S n)" + proof (rule measure_nested_Union) + show "?S n \ lmeasurable" for n + by (simp add: False fmeasurable.finite_UN from_nat_into measD) + show "measure lebesgue (?S n) \ B" for n + by (metis (mono_tags, lifting) B False finite_atMost finite_imageI from_nat_into image_iff subsetI) + show "?S n \ ?S (Suc n)" for n + by force + qed + then obtain N where N: "\n. n \ N \ dist (measure lebesgue (?S n)) (measure lebesgue (\n. ?S n)) < e" + using metric_LIMSEQ_D \e > 0\ by blast + show ?thesis + proof + show "from_nat_into \ ` {..N} \ \" + by (auto simp: False from_nat_into) + have eq: "(\n. \k\n. from_nat_into \ k) = (\\)" + using \countable \\ False + by (auto intro: from_nat_into dest: from_nat_into_surj [OF \countable \\]) + show "measure lebesgue (\\) - e < measure lebesgue (UNION {..N} (from_nat_into \))" + using N [OF order_refl] + by (auto simp: eq algebra_simps dist_norm) + qed auto +qed + subsection\Integral bounds\ lemma set_integral_norm_bound: diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Apr 16 05:34:25 2018 +0000 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Apr 16 15:00:46 2018 +0100 @@ -978,8 +978,24 @@ and lmeasurable_box [iff]: "box a b \ lmeasurable" by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) +lemma fmeasurable_compact: "compact S \ S \ fmeasurable lborel" + using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact) + lemma lmeasurable_compact: "compact S \ S \ lmeasurable" - using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact) + using fmeasurable_compact by (force simp: fmeasurable_def) + +lemma measure_frontier: + "bounded S \ measure lebesgue (frontier S) = measure lebesgue (closure S) - measure lebesgue (interior S)" + using closure_subset interior_subset + by (auto simp: frontier_def fmeasurable_compact intro!: measurable_measure_Diff) + +lemma lmeasurable_closure: + "bounded S \ closure S \ lmeasurable" + by (simp add: lmeasurable_compact) + +lemma lmeasurable_frontier: + "bounded S \ frontier S \ lmeasurable" + by (simp add: compact_frontier_bounded lmeasurable_compact) lemma lmeasurable_open: "bounded S \ open S \ S \ lmeasurable" using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open) diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Mon Apr 16 05:34:25 2018 +0000 +++ b/src/HOL/Analysis/Measure_Space.thy Mon Apr 16 15:00:46 2018 +0100 @@ -1749,6 +1749,8 @@ using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset) qed +subsection\Measurable sets formed by unions and intersections\ + lemma fmeasurable_Diff: "A \ fmeasurable M \ B \ sets M \ A - B \ fmeasurable M" using fmeasurableI2[of A M "A - B"] by auto @@ -1882,15 +1884,20 @@ "finite F \ (\S. S \ F \ S \ sets M) \ measure M (\F) \ (\S\F. measure M S)" using measure_UNION_le[of F "\x. x" M] by simp +text\Version for indexed union over a countable set\ lemma assumes "countable I" and I: "\i. i \ I \ A i \ fmeasurable M" - and bound: "\I'. I' \ I \ finite I' \ measure M (\i\I'. A i) \ B" and "0 \ B" + and bound: "\I'. I' \ I \ finite I' \ measure M (\i\I'. A i) \ B" shows fmeasurable_UN_bound: "(\i\I. A i) \ fmeasurable M" (is ?fm) and measure_UN_bound: "measure M (\i\I. A i) \ B" (is ?m) proof - + have "B \ 0" + using bound by force have "?fm \ ?m" proof cases - assume "I = {}" with \0 \ B\ show ?thesis by simp + assume "I = {}" + with \B \ 0\ show ?thesis + by simp next assume "I \ {}" have "(\i\I. A i) = (\i. (\n\i. A (from_nat_into I n)))" @@ -1918,6 +1925,58 @@ then show ?fm ?m by auto qed +text\Version for big union of a countable set\ +lemma + assumes "countable \" + and meas: "\D. D \ \ \ D \ fmeasurable M" + and bound: "\\. \\ \ \; finite \\ \ measure M (\\) \ B" + shows fmeasurable_Union_bound: "\\ \ fmeasurable M" (is ?fm) + and measure_Union_bound: "measure M (\\) \ B" (is ?m) +proof - + have "B \ 0" + using bound by force + have "?fm \ ?m" + proof (cases "\ = {}") + case True + with \B \ 0\ show ?thesis + by auto + next + case False + then obtain D :: "nat \ 'a set" where D: "\ = range D" + using \countable \\ uncountable_def by force + have 1: "\i. D i \ fmeasurable M" + by (simp add: D meas) + have 2: "\I'. finite I' \ measure M (\x\I'. D x) \ B" + by (simp add: D bound image_subset_iff) + show ?thesis + unfolding D + by (intro conjI fmeasurable_UN_bound [OF _ 1 2] measure_UN_bound [OF _ 1 2]) auto + qed + then show ?fm ?m by auto +qed + +text\Version for indexed union over the type of naturals\ +lemma + fixes S :: "nat \ 'a set" + assumes S: "\i. S i \ fmeasurable M" and B: "\n. measure M (\i\n. S i) \ B" + shows fmeasurable_countable_Union: "(\i. S i) \ fmeasurable M" + and measure_countable_Union_le: "measure M (\i. S i) \ B" +proof - + have mB: "measure M (\i\I. S i) \ B" if "finite I" for I + proof - + have "(\i\I. S i) \ (\i\Max I. S i)" + using Max_ge that by force + then have "measure M (\i\I. S i) \ measure M (\i \ Max I. S i)" + by (rule measure_mono_fmeasurable) (use S in \blast+\) + then show ?thesis + using B order_trans by blast + qed + show "(\i. S i) \ fmeasurable M" + by (auto intro: fmeasurable_UN_bound [OF _ S mB]) + show "measure M (\n. S n) \ B" + by (auto intro: measure_UN_bound [OF _ S mB]) +qed + lemma measure_diff_le_measure_setdiff: assumes "S \ fmeasurable M" "T \ fmeasurable M" shows "measure M S - measure M T \ measure M (S - T)" diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Mon Apr 16 05:34:25 2018 +0000 +++ b/src/HOL/Analysis/Starlike.thy Mon Apr 16 15:00:46 2018 +0100 @@ -8421,6 +8421,83 @@ apply (simp add: adjoint_works assms(1) inner_commute) by (metis adjoint_works all_zero_iff assms(1) inner_commute) +subsection\ A non-injective linear function maps into a hyperplane.\ + +lemma linear_surj_adj_imp_inj: + fixes f :: "'m::euclidean_space \ 'n::euclidean_space" + assumes "linear f" "surj (adjoint f)" + shows "inj f" +proof - + have "\x. y = adjoint f x" for y + using assms by (simp add: surjD) + then show "inj f" + using assms unfolding inj_on_def image_def + by (metis (no_types) adjoint_works euclidean_eqI) +qed + +(*http://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map*) +lemma surj_adjoint_iff_inj [simp]: + fixes f :: "'m::euclidean_space \ 'n::euclidean_space" + assumes "linear f" + shows "surj (adjoint f) \ inj f" +proof + assume "surj (adjoint f)" + then show "inj f" + by (simp add: assms linear_surj_adj_imp_inj) +next + assume "inj f" + have "f -` {0} = {0}" + using assms \inj f\ linear_0 linear_injective_0 by fastforce + moreover have "f -` {0} = range (adjoint f)\<^sup>\" + by (intro ker_orthogonal_comp_adjoint assms) + ultimately have "range (adjoint f)\<^sup>\\<^sup>\ = UNIV" + by (metis orthogonal_comp_null) + then show "surj (adjoint f)" + by (simp add: adjoint_linear \linear f\ subspace_linear_image orthogonal_comp_self) +qed + +lemma inj_adjoint_iff_surj [simp]: + fixes f :: "'m::euclidean_space \ 'n::euclidean_space" + assumes "linear f" + shows "inj (adjoint f) \ surj f" +proof + assume "inj (adjoint f)" + have "(adjoint f) -` {0} = {0}" + by (metis \inj (adjoint f)\ adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV) + then have "(range(f))\<^sup>\ = {0}" + by (metis (no_types, hide_lams) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero) + then show "surj f" + by (metis \inj (adjoint f)\ adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj) +next + assume "surj f" + then have "range f = (adjoint f -` {0})\<^sup>\" + by (simp add: adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint) + then have "{0} = adjoint f -` {0}" + using \surj f\ adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force + then show "inj (adjoint f)" + by (simp add: \surj f\ adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj) +qed + +proposition linear_singular_into_hyperplane: + fixes f :: "'n::euclidean_space \ 'n" + assumes "linear f" + shows "\ inj f \ (\a. a \ 0 \ (\x. a \ f x = 0))" (is "_ = ?rhs") +proof + assume "\inj f" + then show ?rhs + using all_zero_iff + by (metis (no_types, hide_lams) adjoint_clauses(2) adjoint_linear assms linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj) +next + assume ?rhs + then show "\inj f" + by (metis assms linear_injective_isomorphism all_zero_iff) +qed + +lemma linear_singular_image_hyperplane: + fixes f :: "'n::euclidean_space \ 'n" + assumes "linear f" "\inj f" + obtains a where "a \ 0" "\S. f ` S \ {x. a \ x = 0}" + using assms by (fastforce simp add: linear_singular_into_hyperplane) end