This instance will be upgraded to Heptapod 0.31.0 (final) on 2022-05-24 at 14:00 UTC+2 (a few minutes of down time)

Commit ba24e36e authored by Alexander Bentkamp's avatar Alexander Bentkamp
Browse files

Remove unnessecary argument from witness_submatrix

parent 71767e8d023f
......@@ -285,7 +285,7 @@ context deep_model_correct_params_y
begin
definition witness_submatrix where
"witness_submatrix j f = submatrix (A' f) rows_with_1 rows_with_1"
"witness_submatrix f = submatrix (A' f) rows_with_1 rows_with_1"
lemma polyfun_tensor_deep_model:
......@@ -326,7 +326,7 @@ qed
lemma polyfun_submatrix_deep_model:
assumes "i < r ^ N_half"
assumes "j < r ^ N_half"
shows "polyfun {..<weight_space_dim} (\<lambda>f. witness_submatrix y f $$ (i,j))"
shows "polyfun {..<weight_space_dim} (\<lambda>f. witness_submatrix f $$ (i,j))"
unfolding witness_submatrix_def
proof (rule polyfun_submatrix)
have 1:"\<And>f. remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
......@@ -344,16 +344,16 @@ proof (rule polyfun_submatrix)
qed
lemma polyfun_det_deep_model:
shows "polyfun {..<weight_space_dim} (\<lambda>f. det (witness_submatrix y f))"
shows "polyfun {..<weight_space_dim} (\<lambda>f. det (witness_submatrix f))"
proof (rule polyfun_det)
fix f
have "remove_weights (insert_weights (deep_model_l rs) f) = deep_model_l rs"
using remove_insert_weights by metis
show "witness_submatrix y f \<in> carrier\<^sub>m (r ^ N_half) (r ^ N_half)"
show "witness_submatrix f \<in> carrier\<^sub>m (r ^ N_half) (r ^ N_half)"
unfolding witness_submatrix_def apply (rule mat_carrierI) unfolding dim_submatrix[unfolded set_le_in]
unfolding dims_A'_pow[unfolded weight_space_dim_def] using card_rows_with_1 dims_Aw'_pow by simp_all
show "\<And>i j. i < r ^ N_half \<Longrightarrow> j < r ^ N_half \<Longrightarrow> polyfun {..<weight_space_dim} (\<lambda>f. witness_submatrix y f $$ (i, j))"
show "\<And>i j. i < r ^ N_half \<Longrightarrow> j < r ^ N_half \<Longrightarrow> polyfun {..<weight_space_dim} (\<lambda>f. witness_submatrix f $$ (i, j))"
using polyfun_submatrix_deep_model by blast
qed
......
......@@ -15,7 +15,7 @@ and "\<And>x. insertion x p \<noteq> 0 \<Longrightarrow> r ^ N_half \<le> cprank
proof -
assume assumption:"\<And>p. p \<noteq> 0 \<Longrightarrow> vars p \<subseteq> {..<weight_space_dim} \<Longrightarrow>
(\<And>x. insertion x p \<noteq> 0 \<Longrightarrow> r ^ N_half \<le> cprank (A x)) \<Longrightarrow> thesis"
obtain p where p_def:"\<And>x. insertion x p = Determinant.det (witness_submatrix y x)" and
obtain p where p_def:"\<And>x. insertion x p = Determinant.det (witness_submatrix x)" and
vars_p:"vars p \<subseteq> {..<weight_space_dim}"
using polyfun_det_deep_model[unfolded polyfun_def] by auto
then have "insertion witness_weights p \<noteq> 0"
......@@ -25,11 +25,11 @@ proof -
have "\<And>x. insertion x p \<noteq> 0 \<Longrightarrow> r ^ N_half \<le> cprank (A x)"
proof -
fix x assume "insertion x p \<noteq> 0"
then have "Determinant.det (witness_submatrix y x) \<noteq> 0" using p_def by auto
then have "Determinant.det (witness_submatrix x) \<noteq> 0" using p_def by auto
have 0:"weight_space_dim \<le> length (map x [0..<weight_space_dim])" by auto
have "r ^ N_half \<le> mrank (A' x)"
using vec_space.rank_gt_minor[OF mat_carrierI[OF dims_A'_pow, unfolded weight_space_dim_def]
`Determinant.det (witness_submatrix y x) \<noteq> 0`[unfolded witness_submatrix_def]]
`Determinant.det (witness_submatrix x) \<noteq> 0`[unfolded witness_submatrix_def]]
card_rows_with_1[unfolded dims_Aw'_pow] by (metis (no_types, lifting) Collect_cong dims_A'_pow(1))
also have "... \<le> cprank (A x)" using matrix_rank_le_cp_rank A'_def by auto
finally show "r ^ N_half \<le> cprank (A x)" .
......
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