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