# Theory Lebesgue_Zero_Set

theory Lebesgue_Zero_Set
imports Lebesgue_Functional MPoly_Type_Univariate
```(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section ‹Lebesgue Measure of Polynomial Zero Sets›

theory Lebesgue_Zero_Set
imports
Polynomials.More_MPoly_Type
Lebesgue_Functional
Polynomials.MPoly_Type_Univariate
begin

lemma measurable_insertion [measurable]:
assumes "vars p ⊆ {..<n}"
shows "(λf. insertion f p) ∈ borel_measurable (lborel_f n)"
using assms proof (induction p rule:mpoly_induct)
case (monom m a)
then show ?case
proof (cases "a = 0")
case True
show ?thesis unfolding insertion_single ‹a = 0› MPoly_Type.monom.abs_eq single_zero
zero_mpoly.abs_eq[symmetric] insertion_zero by measurable
next
case False
have "Poly_Mapping.keys m ⊆ {..<n}" using monom by (simp add: False vars_monom_keys)
then show ?thesis using ‹a≠0›
proof (induction m arbitrary:a rule:poly_mapping_induct)
case (single x i a)
then show ?case
proof (cases "i = 0")
case True
show ?thesis unfolding insertion_single ‹i = 0› by simp
next
case False
then show ?thesis unfolding insertion_single apply measurable
using vars_monom_single_cases single False insert_subset lessThan_iff ‹a≠0› by fastforce
qed
next
case (sum m1 m2 x i)
then have "Poly_Mapping.keys m1 ∩ Poly_Mapping.keys m2 = {}" by simp
then have "Poly_Mapping.keys m1 ∪ Poly_Mapping.keys m2 = Poly_Mapping.keys (m1 + m2)" using keys_add by metis
then have 1:"Poly_Mapping.keys m1 ⊆ {..<n}" and 2:"Poly_Mapping.keys m2 ⊆ {..<n}" using sum.prems by auto
show ?case unfolding MPoly_Type.mult_monom[of m1 a m2 1,simplified,symmetric]
insertion_mult using sum.IH(1)[OF 1 ‹a≠0›] sum.IH(2)[OF 2, of 1, simplified] by measurable
qed
qed
next
case (sum p1 p2 m a)
then have "(λf. insertion f p1) ∈ borel_measurable (lborel_f n)"
"(λf. insertion f p2) ∈ borel_measurable (lborel_f n)"
using vars_add_monom[OF sum.hyps]  le_sup_iff by blast+
then show ?case unfolding insertion_add by measurable
qed

text ‹This proof follows Richard Caron and Tim Traynor, "The zero set of a polynomial"
http://www1.uwindsor.ca/math/sites/uwindsor.ca.math/files/05-03.pdf›

lemma lebesgue_mpoly_zero_set:
fixes p::"real mpoly"
assumes "p ≠ 0" "vars p ⊆ {..<n}"
shows "{f∈space (lborel_f n). insertion f p = 0} ∈ null_sets (lborel_f n)"
using assms proof (induction n arbitrary:p)
case 0
then have "vars p = {}" by simp then have "⋀f. insertion f p = MPoly_Type.coeff p 0"
unfolding insertion_trivial[symmetric] using insertion_irrelevant_vars by blast
have "⋀m. m≠0 ⟹ MPoly_Type.coeff p m = 0"
proof (rule ccontr)
fix m::"nat ⇒⇩0 nat" assume "m≠0" "MPoly_Type.coeff p m ≠ 0"
then obtain v where "Poly_Mapping.lookup m v ≠ 0" using aux by auto
then have "v∈vars p" unfolding More_MPoly_Type.vars_def using ‹MPoly_Type.coeff p m ≠ 0›
by (meson UN_I coeff_keys lookup_not_eq_zero_eq_in_keys)
then show False using ‹vars p = {}› by auto
qed
then have "MPoly_Type.coeff p 0 ≠ 0" using ‹p ≠ 0›
by (metis coeff_all_0)
then have "{f. insertion f p = 0} = {}" using ‹⋀f. insertion f p = MPoly_Type.coeff p 0› by auto
then show ?case by auto
next
case (Suc n p)

text ‹Show that N is finite:›
then have "extract_var p n ≠ 0" using reduce_nested_mpoly_0
by (metis reduce_nested_mpoly_extract_var)
let ?q = "λj. MPoly_Type.coeff (extract_var p n) j"
obtain j where "?q j ≠ 0" using ‹extract_var p n ≠ 0›
by (metis coeff_all_0)
then have "finite {x. insertion (λ_. x) (?q j) = 0}"
using univariate_mpoly_roots_finite[OF vars_coeff_extract_var] by metis
then have "finite (⋂j. {x. insertion (λ_. x) (?q j) = 0})" by auto
moreover have "{x. ∀j. insertion (λ_. x) (?q j) = 0} = (⋂j. {x. insertion (λv. x) (?q j) = 0})" by blast
ultimately have "finite {x. ∀j. insertion (λ_. x) (?q j) = 0}" by metis

define p_fix1 where "p_fix1 x1 = replace_coeff (insertion (λ_. x1)) (extract_var p n)" for x1
define N where "N = {x1. p_fix1 x1 = 0}"
have "N ⊆ {x. ∀j. insertion (λ_. x) (?q j) = 0}"
proof
fix x assume "x∈N"
then have "p_fix1 x = 0" using N_def by auto
then have "⋀m. MPoly_Type.coeff (p_fix1 x) m = 0" by (metis More_MPoly_Type.coeff_monom monom_zero when_def)
have "⋀j. insertion (λ_. x) (?q j) = 0"
using ‹⋀m. MPoly_Type.coeff (p_fix1 x) m = 0›[unfolded p_fix1_def coeff_replace_coeff[of "insertion (λ_. x)", OF insertion_zero]]
by metis
then show "x ∈ {x. ∀j. insertion (λ_. x) (MPoly_Type.coeff (extract_var p n) j) = 0}" by blast
qed
then have "finite N" by (simp add: ‹finite {x. ∀j. insertion (λ_. x) (MPoly_Type.coeff (extract_var p n) j) = 0}› finite_subset)

text ‹Use the IH:›

define A where "A = {f∈space (lborel_f (Suc n)). insertion f p = 0}"

have "⋀x1. vars (p_fix1 x1) ⊆ {..<n}"
proof -
fix x1
have "vars (extract_var p n) ⊆ {..<n}"
using ‹vars p ⊆ {..<Suc n}› lessThan_Suc v_not_in_vars_extract_var vars_extract_var_subset by fastforce
then show "vars (p_fix1 x1) ⊆ {..<n}" unfolding p_fix1_def
using vars_replace_coeff[of "insertion (λ_. x1)", OF insertion_zero] by blast
qed
have set_eq:"⋀x1. {x ∈ space (lborel_f n). x(n := x1) ∈ A} = {f ∈ space (lborel_f n). insertion f (p_fix1 x1) = 0}"
proof -
fix x1
show "{x∈space (lborel_f n). x(n := x1) ∈ A} = {f∈space (lborel_f n). insertion f (p_fix1 x1) = 0}"
proof (rule subset_antisym;rule subsetI)
fix x assume "x ∈ {x∈space (lborel_f n). x(n := x1) ∈ A}"
then have "insertion (x(n := x1)) p = 0" "x ∈ space (lborel_f n)"
using A_def by auto
then have "insertion x (p_fix1 x1) = 0" unfolding p_fix1_def
unfolding replace_coeff_extract_var_cong[of "λ_. x1" n "x(n := x1)" p, OF fun_upd_same[symmetric]]
using insertion_replace_coeff[of "x(n := x1)"]
using  insertion_irrelevant_vars[of "replace_coeff (insertion (x(n := x1))) (extract_var p n)" x "x(n := x1)"]
vars_replace_coeff fun_upd_other insertion_zero reduce_nested_mpoly_extract_var subset_eq
v_not_in_vars_extract_var by metis
then show "x ∈ {f∈space (lborel_f n). insertion f (p_fix1 x1) = 0}" using ‹x ∈ space (lborel_f n)› by blast
next
fix f assume "f ∈ {f∈space (lborel_f n). insertion f (p_fix1 x1) = 0}"
then have "f∈space (lborel_f n)" "insertion f (p_fix1 x1) = 0" by auto
have "insertion (f(n := x1)) p = 0" using ‹insertion f (p_fix1 x1) = 0›[unfolded p_fix1_def]
insertion_replace_coeff insertion_irrelevant_vars replace_coeff_extract_var_cong
by (metis (no_types, lifting) ‹insertion f (p_fix1 x1) = 0› ‹vars (p_fix1 x1) ⊆ {..<n}›
fun_upd_other fun_upd_same lessThan_iff order_less_irrefl p_fix1_def reduce_nested_mpoly_extract_var subsetCE)
then have "f(n := x1) ∈ A" unfolding A_def using space_lborel_add_dim
using ‹f ∈ space (lborel_f n)› lborel_f_def mem_Collect_eq by blast
then show "f ∈ {f∈space (lborel_f n). f(n := x1) ∈ A}" using ‹f ∈ space (lborel_f n)› by auto
qed
qed

have "⋀x1. x1∈N ⟹ {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)"
and emeasure_in_N: "⋀x1. x1∈N ⟹ emeasure (lborel_f n) {x∈space (lborel_f n). x(n := x1) ∈ A} = emeasure (lborel_f n) (space (lborel_f n))"
proof -
fix x1 assume "x1∈N"
then have "p_fix1 x1 = 0" using N_def by auto
then have "⋀f. insertion f (p_fix1 x1) = 0" using insertion_zero by auto
then have "{f ∈ space (lborel_f n). insertion f (p_fix1 x1) = 0} = space (lborel_f n)" by simp
show "{x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)" unfolding set_eq
by (simp add: ‹{f ∈ space (lborel_f n). insertion f (p_fix1 x1) = 0} = space (lborel_f n)›)
show "emeasure (lborel_f n) {x∈space (lborel_f n). x(n := x1) ∈ A} = emeasure (lborel_f n) (space (lborel_f n))"
unfolding set_eq
by (simp add: ‹{f ∈ space (lborel_f n). insertion f (p_fix1 x1) = 0} = space (lborel_f n)›)
qed

have emeasure_not_in_N: "⋀x1. x1∉N ⟹ emeasure (lborel_f n) {x∈space (lborel_f n). x(n := x1) ∈ A} = 0"
and "⋀x1. x1∉N ⟹ {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)"
proof -
fix x1 assume "x1∉N"
then have "p_fix1 x1 ≠ 0" using p_fix1_def N_def by auto
then have "emeasure (lborel_f n) {f∈space (lborel_f n). insertion f (p_fix1 x1) = 0} = 0"
"{f∈space (lborel_f n). insertion f (p_fix1 x1) = 0} ∈ sets (lborel_f n)"
using Suc.IH[OF ‹p_fix1 x1 ≠ 0›] ‹⋀x1. vars (p_fix1 x1) ⊆ {..<n}› by auto
then show "emeasure (lborel_f n) {x∈space (lborel_f n). x(n := x1) ∈ A} = 0"
"{x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)"
using ‹{f∈space (lborel_f n). insertion f (p_fix1 x1) = 0} ∈ sets (lborel_f n)›
‹emeasure (lborel_f n) {f∈space (lborel_f n). insertion f (p_fix1 x1) = 0} = 0›
using set_eq
by auto
qed

have "N ∈ null_sets lborel" using ‹finite N› finite_imp_null_set_lborel by blast
have ae_zero: "AE x1 in lborel. emeasure (lborel_f n) {x ∈ space (lborel_f n). x(n := x1) ∈ A} = 0"
apply (rule AE_I'[OF ‹N ∈ null_sets lborel›])
using ‹⋀x1. x1∉N ⟹ emeasure (lborel_f n) {x∈space (lborel_f n). x(n := x1) ∈ A} = 0›
by force

have measurable: "(λx1. emeasure (lborel_f n) {x ∈ space (lborel_f n). x(n := x1) ∈ A}) ∈ borel_measurable lborel"
proof (rule borel_measurableI)
let ?f = "(λx1. emeasure (lborel_f n) {x ∈ space (lborel_f n). x(n := x1) ∈ A})"
fix S::"ennreal set" assume "open S"
have 0:"0∈S ⟹ - N ⊆ ?f -` S"
using emeasure_not_in_N by auto
have 1:"emeasure (lborel_f n) (space (lborel_f n)) ∈ S ⟹ N ⊆ ?f -` S"
using emeasure_in_N by auto
have 2:"0∉S ⟹ ?f -` S ⊆ N" using emeasure_not_in_N by fastforce
have 3:"emeasure (lborel_f n) (space (lborel_f n)) ∉ S ⟹ ?f -` S ⊆ -N" using emeasure_in_N by auto
have "?f -` S = {} ∨ ?f -` S = N ∨ ?f -` S = UNIV ∨ ?f -` S = - N"
apply (cases "0∈S"; cases "emeasure (lborel_f n) (space (lborel_f n)) ∉ S")
using 0 1 2 3 by auto
then show "?f -` S  ∩ space lborel ∈ sets lborel"
using ‹finite N› finite_imp_null_set_lborel borel_comp null_setsD2 sets_lborel by fastforce
qed

have "A ∈ sets (lborel_f (Suc n))" unfolding A_def
using pred_eq_const1[OF measurable_insertion[OF ‹vars p ⊆ {..<Suc n}›]] pred_def by force
then have in_sets: "{f ∈ space (lborel_f (Suc n)). insertion f p = 0} ∈ sets (lborel_f (Suc n))" using A_def by metis
have "⋀x1. {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)"
using ‹⋀x1. x1∈N ⟹ {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)›
‹⋀x1. x1∉N ⟹ {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)› by auto
have "emeasure (lborel_f (Suc n)) A = ∫⇧+ y. emeasure (lborel_f n) {x ∈ space (lborel_f n). x(n := y) ∈ A} ∂lborel"
using emeasure_lborel_f_Suc[OF ‹A ∈ sets (lborel_f (Suc n))›]
‹⋀x1. {x∈space (lborel_f n). x(n := x1) ∈ A} ∈ sets (lborel_f n)› by blast
also have "... = 0"
using nn_integral_0_iff_AE[OF measurable] ae_zero by blast
finally have "emeasure (lborel_f (Suc n)) A = 0" by auto
then show ?case unfolding null_sets_def using in_sets A_def by blast
qed

end
```