Commit 41973964 authored by blanchet's avatar blanchet
Browse files

removed redundant theorem (and theory file) + fixed a few paths + tuning

parent d59baab37801
......@@ -163,7 +163,6 @@ next
unfolding semigroup_add_class.add.assoc ab_semigroup_add_class.add.commute[of "x1 * x2" a]
by blast
have "output_size m = x2" using Conv.prems(2) \<open>x = (x1, x2)\<close> valid_net.cases by fastforce
show "\<And>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 \<in> carrier\<^sub>m x1 (output_size m)" unfolding `output_size m = x2` using dim_extract_matrix
using mat_carrierI by (metis (no_types, lifting))
......
......@@ -3,8 +3,7 @@
section \<open>Fundamental Theorem of Network Capacity\<close>
theory DL_Fundamental_Theorem_Network_Capacity
imports DL_Rank_CP_Rank DL_Deep_Model_Poly Lebesgue_Zero_Set DL_Rank_Submatrix "~~/src/HOL/Probability/Complete_Measure" DL_Shallow_Model
DL_Missing_Complete_Measure
imports DL_Rank_CP_Rank DL_Deep_Model_Poly Lebesgue_Zero_Set DL_Rank_Submatrix "~~/src/HOL/Analysis/Complete_Measure" DL_Shallow_Model
begin
context deep_model_correct_params_y
......
(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section \<open>Missing Lemmas of Complete\_Measure\<close>
theory DL_Missing_Complete_Measure
imports "~~/src/HOL/Probability/Complete_Measure"
begin
lemma null_sets_completion_subset:
assumes "A \<in> null_sets (completion M)" "B \<subseteq> A"
shows "B \<in> null_sets (completion M)"
proof -
obtain N where "N \<in> null_sets M" "null_part M A \<subseteq> N"
using null_part[OF null_setsD2[OF assms(1)]] by blast
then have "B \<subseteq> main_part M A \<union> N"
using main_part_null_part_Un[OF null_setsD2[OF assms(1)]] `B \<subseteq> A` by auto
have "main_part M A \<in> null_sets M" using emeasure_completion[OF null_setsD2[OF assms(1)]]
by (metis assms(1) main_part_sets null_setsD1 null_setsD2 null_setsI)
then have "main_part M A \<union> N \<in> null_sets M" using \<open>N \<in> null_sets M\<close> by blast
then show ?thesis using null_sets_completion
by (metis \<open>B \<subseteq> main_part M A \<union> N\<close> assms(1) assms(2) emeasure_Un_null_set le_iff_sup null_setsD1 null_setsI)
qed
end
......@@ -14,8 +14,8 @@ definition shallow_model where
"shallow_model Y Z M N = Conv (Y,Z) (shallow_model' Z M N)"
lemma valid_shallow_model': "valid_net (shallow_model' Z M N)"
apply (induction N) unfolding shallow_model'.simps
by (simp add: valid_net.intros, metis shallow_model'.elims shallow_model'.simps(1) valid_net.intros output_size.simps)
apply (induction N) unfolding shallow_model'.simps
by (simp add: valid_net.intros, metis shallow_model'.elims shallow_model'.simps(1) valid_net.intros output_size.simps)
lemma output_size_shallow_model': "output_size (shallow_model' Z M N) = Z"
apply (induction N) unfolding shallow_model'.simps using output_size.simps by simp_all
......
......@@ -3,7 +3,7 @@
section \<open>Alternative Lebesgue Measure Definition\<close>
theory Lebesgue_Functional
imports "~~/src/HOL/Probability/Lebesgue_Measure" "~~/src/HOL/Topological_Spaces"
imports "~~/src/HOL/Analysis/Lebesgue_Measure" "~~/src/HOL/Topological_Spaces"
begin
text \<open>Lebesgue\_Measure.lborel is defined on the typeclass euclidean\_space, which does not allow the
......
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