Commit cf03a365 authored by Max W. Haslbeck's avatar Max W. Haslbeck
Browse files

add lemma with bounds for all numbers in GSO

parent b50e1734e10d
......@@ -544,7 +544,7 @@ section \<open>Bounds on $\sigma$ and $\mu'$\<close>
context gram_schmidt_fs_int
begin
lemma A_mu':
lemma A_\<mu>':
assumes "i < m" "j \<le> i"
shows "(\<mu>' i j)\<^sup>2 \<le> A ^ (3 * Suc j)"
proof -
......@@ -579,7 +579,7 @@ qed
lemma A_\<sigma>:
assumes "i < m" "j \<le> i" "l \<le> j"
shows "\<bar>\<sigma> l i j\<bar> \<le> of_nat l * A ^ (2 * l + 2)"
shows "\<bar>\<sigma> l i j\<bar> \<le> of_nat l * A ^ (2 * l + 2)"
proof -
have 1: "\<bar>d l\<bar> = d l"
using Gramian_determinant(2) assms by (intro abs_of_pos) auto
......@@ -624,6 +624,101 @@ proof -
by simp
qed
lemma leq_squared: "(z::int) \<le> z\<^sup>2"
proof (cases "0 < z")
case True
then show ?thesis
by (auto intro!: self_le_power)
next
case False
then have "z \<le> 0"
by (simp)
also have "0 \<le> z\<^sup>2"
by (auto)
finally show ?thesis
by simp
qed
lemma abs_leq_squared: "\<bar>z::int\<bar> \<le> z\<^sup>2"
using leq_squared[of "\<bar>z\<bar>"] by auto
lemma combined_size_bound_integer:
assumes x: "x \<in> {fs ! i $ j | i j. i < m \<and> j < n}
\<union> {\<mu>' i j | i j. j \<le> i \<and> i < m}
\<union> {\<sigma> l i l | i j l. i < m \<and> j \<le> i \<and> l \<le> j}"
(is "x \<in> ?fs \<union> ?\<mu>' \<union> ?\<sigma>")
and m: "m \<noteq> 0"
shows "\<bar>x\<bar> \<le> of_nat m * A ^ (3 * Suc m)"
proof -
let ?m = "(of_nat m)::'a::trivial_conjugatable_linordered_field"
have [simp]: "1 \<le> ?m"
using m by (metis Num.of_nat_simps One_nat_def Suc_leI neq0_conv of_nat_mono)
have [simp]: "\<bar>(of_int z)::'a::trivial_conjugatable_linordered_field\<bar> \<le> (of_int z)\<^sup>2" for z
using abs_leq_squared by (metis of_int_abs of_int_le_iff of_int_power)
have "\<bar>fs ! i $v j\<bar> \<le> of_nat m * A ^ (3 * Suc m)" if "i < m" "j < n" for i j
proof -
have "\<bar>fs ! i $v j\<bar> \<le> \<bar>fs ! i $v j\<bar>\<^sup>2"
by (rule Ints_cases[of "fs ! i $v j"]) (use fs_int that in auto)
also have "\<bar>fs ! i $v j\<bar>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2"
using that by (intro vec_le_sq_norm) (auto)
also have "... \<le> 1 * A"
using A_fs that by auto
also have "\<dots> \<le> of_nat m * A ^ (3 * Suc m)"
using m A_1 by (intro mult_mono) (auto intro!: mult_mono self_le_power)
finally show ?thesis
by (auto)
qed
then have "\<bar>x\<bar> \<le> of_nat m * A ^ (3 * Suc m)" if "x \<in> ?fs"
using that by auto
moreover have "\<bar>x\<bar> \<le> of_nat m * A ^ (3 * Suc m)" if "x \<in> ?\<mu>'"
proof -
have "\<bar>\<mu>' i j\<bar> \<le> of_nat m * A ^ (3 + 3 * m)" if "j \<le> i" "i < m" for i j
proof -
have "\<mu>' i j \<in> \<int>"
unfolding \<mu>'_def using that Gramian_determinant_mu_ints by auto
then have "\<bar>\<mu>' i j\<bar> \<le> (\<mu>' i j)\<^sup>2"
by (rule Ints_cases[of "\<mu>' i j"]) auto
also have "\<dots> \<le> A ^ (3 * Suc j)"
using that A_\<mu>' by auto
also have "\<dots> \<le> 1 * A ^ (3 * Suc m)"
using that assms A_1 by (auto intro!: power_increasing)
also have "\<dots> \<le> of_nat m * A ^ (3 * Suc m)"
using A_ge_0 assms zero_le_power by (intro mult_mono) auto
finally show ?thesis
by auto
qed
then show ?thesis
using that by auto
qed
moreover have "\<bar>x\<bar> \<le> of_nat m * A ^ (3 * Suc m)" if "x \<in> ?\<sigma>"
proof -
have "\<bar>\<sigma> l i l\<bar> \<le> of_nat m * A ^ (3 + 3 * m)" if "i < m" "j \<le> i" "l \<le> j" for i j l
proof -
have "\<bar>\<sigma> l i l\<bar> \<le> of_nat l * A ^ (2 * l + 2)"
using that A_\<sigma> by auto
also have "\<dots> \<le> of_nat m * A ^ (2 * l + 2)"
using that A_ge_0 assms zero_le_power by (intro mult_mono) auto
also have "\<dots> \<le> of_nat m * A ^ (3 * Suc m)"
proof -
have "A ^ (2 * l + 2) \<le> A ^ (3 * Suc m)"
using that assms A_1 by (intro power_increasing) (auto intro!: power_increasing)
then show ?thesis
using that assms A_1 by (intro mult_mono) (auto)
qed
finally show ?thesis
by simp
qed
then show ?thesis
using that by (auto)
qed
ultimately show ?thesis
using assms by auto
qed
(* "x \<noteq> 0 \<Longrightarrow> log 2 \<bar>x\<bar> \<le> 2 * m * log 2 A + m + log 2 m" (is "_ \<Longrightarrow> ?l1 \<le> ?b1")
"x \<noteq> 0 \<Longrightarrow> log 2 \<bar>x\<bar> \<le> 4 * m * log 2 (M * n) + m + log 2 m" (is "_ \<Longrightarrow> _ \<le> ?b2") *)
end (* gram_schmidt_fs_int *)
section \<open>Calculate $g_i' = d_i g_i$\<close>
......@@ -986,7 +1081,7 @@ qed
end
value (code) "let v = map vec_of_list [[1,2,3],[4,5,6],[7,8,10]] in (gso_array.gso'_array (d\<mu>_impl v) v, d\<mu>_impl v)"
value (code) "gram_schmidt 3 (map vec_of_list [[1::int,2,3],[4,5,6],[7,8,10]])"
value (code) "let v = map vec_of_list [[1,2,3],[4,5,6],[7,8,10]] in (gso_array.gso_array v)"
value (code) "gram_schmidt 3 (map vec_of_list [[1::rat,2,3],[4,5,6],[7,8,10]])"
end
......@@ -423,37 +423,23 @@ lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
by (cases n) (simp_all add: power_gt1_lemma)
text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
proof (induct N)
case 0
then show ?case by simp
next
proof (induction N)
case (Suc N)
then have "a * a^N \<le> 1 * a^n" if "n \<le> N"
using that by (intro mult_mono) auto
then show ?case
apply (auto simp add: le_Suc_eq)
apply (subgoal_tac "a * a^N \<le> 1 * a^n")
apply simp
apply (rule mult_mono)
apply auto
done
qed
using Suc by (auto simp add: le_Suc_eq)
qed (auto)
text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close>
lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
proof (induct N)
case 0
then show ?case by simp
next
proof (induction N)
case (Suc N)
then have "1 * a^n \<le> a * a^N" if "n \<le> N"
using that by (intro mult_mono) (auto simp add: order_trans[OF zero_le_one])
then show ?case
apply (auto simp add: le_Suc_eq)
apply (subgoal_tac "1 * a^n \<le> a * a^N")
apply simp
apply (rule mult_mono)
apply (auto simp add: order_trans [OF zero_le_one])
done
qed
using Suc by (auto simp add: le_Suc_eq)
qed (auto)
lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
using power_decreasing [of 1 "Suc n" a] by simp
......
......@@ -609,6 +609,10 @@ class trivial_conjugatable_ordered_field =
class trivial_conjugatable_linordered_field =
trivial_conjugatable_ordered_field + linordered_field
begin
subclass conjugatable_ring_1_abs_real_line
by (standard) (auto simp add: semiring_normalization_rules)
end
instance rat :: trivial_conjugatable_linordered_field
by (standard, auto)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment