author | Jan Rocnik <jan.rocnik@student.tugraz.at> |
Wed, 26 Oct 2011 11:05:36 +0200 | |
branch | decompose-isar |
changeset 42327 | 4493e57565fd |
parent 42081 | b5a91fb4330c |
permissions | -rw-r--r-- |
neuper@42081 | 1 |
WN110711 |
neuper@42081 | 2 |
HOL/Multivariate_Analysis/ |
neuper@42081 | 3 |
######################### _multi_variate ... nothing else found |
neuper@42081 | 4 |
|
neuper@42081 | 5 |
src$ grep -r "interior " * |
neuper@42081 | 6 |
========================== |
neuper@42081 | 7 |
HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy |
neuper@42081 | 8 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 9 |
definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}" |
neuper@42081 | 10 |
|
neuper@42081 | 11 |
grep -r "definition \"interval" * |
neuper@42081 | 12 |
================================= |
neuper@42081 | 13 |
HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy |
neuper@42081 | 14 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 15 |
definition "interval_bij = (\<lambda> (a::'a,b::'a) (u::'a,v::'a) (x::'a::ordered_euclidean_space). |
neuper@42081 | 16 |
(\<chi>\<chi> i. u$$i + (x$$i - a$$i) / (b$$i - a$$i) * (v$$i - u$$i))::'a)" |
neuper@42081 | 17 |
|
neuper@42081 | 18 |
|
neuper@42081 | 19 |
??? "{a<..<b} \<subseteq> {c..d} \<union> s" ?definition interval? |
neuper@42081 | 20 |
|
neuper@42081 | 21 |
src$ grep -r ".nti.eriv" * |
neuper@42081 | 22 |
========================= |
neuper@42081 | 23 |
1 file except isac: |
neuper@42081 | 24 |
# HOL/Multivariate_Analysis/Derivative.thy |
neuper@42081 | 25 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 26 |
header {* Kurzweil-Henstock Gauge Integration in many dimensions. *} |
neuper@42081 | 27 |
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where |
neuper@42081 | 28 |
"f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)" |
neuper@42081 | 29 |
|
neuper@42081 | 30 |
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where |
neuper@42081 | 31 |
"f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))" |
neuper@42081 | 32 |
|
neuper@42081 | 33 |
definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)" |
neuper@42081 | 34 |
|
neuper@42081 | 35 |
/ |
neuper@42081 | 36 |
========================= |
neuper@42081 | 37 |
HOL/Multivariate_Analysis/Integration.thy |
neuper@42081 | 38 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 39 |
header {* Kurzweil-Henstock Gauge Integration in many dimensions. *} |
neuper@42081 | 40 |
definition "integral i f \<equiv> SOME y. (f has_integral y) i" |
neuper@42081 | 41 |
|
neuper@42081 | 42 |
/ |
neuper@42081 | 43 |
========================= |
neuper@42081 | 44 |
HOL/Multivariate_Analysis/Real_Integration.thy |
neuper@42081 | 45 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 46 |
text{*We follow John Harrison in formalizing the Gauge integral.*} |
neuper@42081 | 47 |
|
neuper@42081 | 48 |
definition Integral :: "real set \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" where |
neuper@42081 | 49 |
"Integral s f k = (f o dest_vec1 has_integral k) (vec1 ` s)" |
neuper@42081 | 50 |
|
neuper@42081 | 51 |
Multivariate_Analysis/L2_Norm.thy:header {* Square root of sum of squares *} |
neuper@42081 | 52 |
|
neuper@42081 | 53 |
|
neuper@42081 | 54 |
################################################################################ |
neuper@42081 | 55 |
### sum |
neuper@42081 | 56 |
################################################################################ |
neuper@42081 | 57 |
src/HOL$ grep -r " sum " * |
neuper@42081 | 58 |
========================== |
neuper@42081 | 59 |
ex/Summation.thy:text {* The formal sum operator. *} |
neuper@42081 | 60 |
ex/Termination.thy:function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
neuper@42081 | 61 |
ex/Termination.thy: "sum i N = (if i > N then 0 else i + sum (Suc i) N)" |
neuper@42081 | 62 |
Isar_Examples/Summation.thy |
neuper@42081 | 63 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
neuper@42081 | 64 |
text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times |
neuper@42081 | 65 |
|
neuper@42081 | 66 |
Series.thy |
neuper@42081 | 67 |
~~~~~~~~~~ |
neuper@42081 | 68 |
header{*Finite Summation and Infinite Series*} |
neuper@42081 | 69 |
|
neuper@42081 | 70 |
Deriv.thy |
neuper@42081 | 71 |
~~~~~~~~~ |
neuper@42081 | 72 |
definition |
neuper@42081 | 73 |
deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" |
neuper@42081 | 74 |
--{*Differentiation: D is derivative of function f at x*} |
neuper@42081 | 75 |
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where |
neuper@42081 | 76 |
"DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" |