Theory Lebesgue_Zero_Set

(* 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