neuper@42081: WN110711
neuper@42081: HOL/Multivariate_Analysis/
neuper@42081: ######################### _multi_variate ... nothing else found
neuper@42081: 
neuper@42081: src$ grep -r "interior " *
neuper@42081: ==========================
neuper@42081: HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
neuper@42081: 
neuper@42081: grep -r "definition \"interval" *
neuper@42081: =================================
neuper@42081: HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: definition "interval_bij = (\<lambda> (a::'a,b::'a) (u::'a,v::'a) (x::'a::ordered_euclidean_space).
neuper@42081:     (\<chi>\<chi> i. u$$i + (x$$i - a$$i) / (b$$i - a$$i) * (v$$i - u$$i))::'a)"
neuper@42081: 
neuper@42081: 
neuper@42081: ??? "{a<..<b} \<subseteq> {c..d} \<union> s" ?definition interval?
neuper@42081: 
neuper@42081: src$ grep -r ".nti.eriv" *
neuper@42081: =========================
neuper@42081: 1 file except isac:
neuper@42081: # HOL/Multivariate_Analysis/Derivative.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
neuper@42081: definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where
neuper@42081:   "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
neuper@42081: 
neuper@42081: definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
neuper@42081:   "f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
neuper@42081: 
neuper@42081: definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
neuper@42081: 
neuper@42081: /
neuper@42081: =========================
neuper@42081: HOL/Multivariate_Analysis/Integration.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
neuper@42081: definition "integral i f \<equiv> SOME y. (f has_integral y) i"
neuper@42081: 
neuper@42081: /
neuper@42081: =========================
neuper@42081: HOL/Multivariate_Analysis/Real_Integration.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: text{*We follow John Harrison in formalizing the Gauge integral.*}
neuper@42081: 
neuper@42081: definition Integral :: "real set \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" where
neuper@42081:   "Integral s f k = (f o dest_vec1 has_integral k) (vec1 ` s)"
neuper@42081: 
neuper@42081: Multivariate_Analysis/L2_Norm.thy:header {* Square root of sum of squares *}
neuper@42081: 
neuper@42081: 
neuper@42081: ################################################################################
neuper@42081: ### sum
neuper@42081: ################################################################################
neuper@42081: src/HOL$ grep -r " sum " *
neuper@42081: ==========================
neuper@42081: ex/Summation.thy:text {* The formal sum operator. *}
neuper@42081: ex/Termination.thy:function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
neuper@42081: ex/Termination.thy:  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
neuper@42081: Isar_Examples/Summation.thy
neuper@42081: ~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@42081: text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times
neuper@42081: 
neuper@42081: Series.thy
neuper@42081: ~~~~~~~~~~
neuper@42081: header{*Finite Summation and Infinite Series*}
neuper@42081: 
neuper@42081: Deriv.thy
neuper@42081: ~~~~~~~~~
neuper@42081: definition
neuper@42081:   deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
neuper@42081:     --{*Differentiation: D is derivative of function f at x*}
neuper@42081:           ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
neuper@42081:   "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"