1.1 --- a/src/Doc/isac/jrocnik/wn-notes.txt Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,76 +0,0 @@
1.4 -WN110711
1.5 -HOL/Multivariate_Analysis/
1.6 -######################### _multi_variate ... nothing else found
1.7 -
1.8 -src$ grep -r "interior " *
1.9 -==========================
1.10 -HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
1.11 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.12 -definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
1.13 -
1.14 -grep -r "definition \"interval" *
1.15 -=================================
1.16 -HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
1.17 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.18 -definition "interval_bij = (\<lambda> (a::'a,b::'a) (u::'a,v::'a) (x::'a::ordered_euclidean_space).
1.19 - (\<chi>\<chi> i. u$$i + (x$$i - a$$i) / (b$$i - a$$i) * (v$$i - u$$i))::'a)"
1.20 -
1.21 -
1.22 -??? "{a<..<b} \<subseteq> {c..d} \<union> s" ?definition interval?
1.23 -
1.24 -src$ grep -r ".nti.eriv" *
1.25 -=========================
1.26 -1 file except isac:
1.27 -# HOL/Multivariate_Analysis/Derivative.thy
1.28 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.29 -header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
1.30 -definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where
1.31 - "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
1.32 -
1.33 -definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
1.34 - "f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
1.35 -
1.36 -definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
1.37 -
1.38 -/
1.39 -=========================
1.40 -HOL/Multivariate_Analysis/Integration.thy
1.41 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.42 -header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
1.43 -definition "integral i f \<equiv> SOME y. (f has_integral y) i"
1.44 -
1.45 -/
1.46 -=========================
1.47 -HOL/Multivariate_Analysis/Real_Integration.thy
1.48 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.49 -text{*We follow John Harrison in formalizing the Gauge integral.*}
1.50 -
1.51 -definition Integral :: "real set \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" where
1.52 - "Integral s f k = (f o dest_vec1 has_integral k) (vec1 ` s)"
1.53 -
1.54 -Multivariate_Analysis/L2_Norm.thy:header {* Square root of sum of squares *}
1.55 -
1.56 -
1.57 -################################################################################
1.58 -### sum
1.59 -################################################################################
1.60 -src/HOL$ grep -r " sum " *
1.61 -==========================
1.62 -ex/Summation.thy:text {* The formal sum operator. *}
1.63 -ex/Termination.thy:function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.64 -ex/Termination.thy: "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
1.65 -Isar_Examples/Summation.thy
1.66 -~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.67 -text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times
1.68 -
1.69 -Series.thy
1.70 -~~~~~~~~~~
1.71 -header{*Finite Summation and Infinite Series*}
1.72 -
1.73 -Deriv.thy
1.74 -~~~~~~~~~
1.75 -definition
1.76 - deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
1.77 - --{*Differentiation: D is derivative of function f at x*}
1.78 - ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
1.79 - "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"