1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/isac/jrocnik/wn-notes.txt	Sun Jul 14 14:48:14 2013 +0200
     1.3 @@ -0,0 +1,76 @@
     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)"