| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 17:30:29 +0000 |
paulson |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 14:31:32 +0200 |
hoelzl |
filters are easier to define with INF on filters.
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 16:45:31 +0100 |
paulson |
new theorem about zero limits
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:16:39 +0200 |
hoelzl |
add limits of power at top and bot
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 07:59:50 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 23:29:33 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:47 +0200 |
hoelzl |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:41 +0200 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:21:01 +0100 |
hoelzl |
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:21:00 +0100 |
hoelzl |
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:58 +0100 |
hoelzl |
move SEQ.thy and Lim.thy to Limits.thy
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:57 +0100 |
hoelzl |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move metric_space to its own theory
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:42 +0100 |
hoelzl |
move topological_space to its own theory
|
file |
diff |
annotate
|
| Wed, 06 Mar 2013 16:56:21 +0100 |
hoelzl |
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file |
diff |
annotate
|
| Wed, 06 Feb 2013 17:57:21 +0100 |
hoelzl |
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:27 +0100 |
hoelzl |
introduce order topology
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 17:16:59 +0100 |
hoelzl |
move eventually_Ball_finite to Limits
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 14:29:09 +0100 |
hoelzl |
add exponential and uniform distributions
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:00:37 +0100 |
hoelzl |
prove tendsto_power_div_exp_0
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:00:31 +0100 |
hoelzl |
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:12 +0100 |
hoelzl |
use filterlim in Lim and SEQ; tuned proofs
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:11 +0100 |
hoelzl |
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:07 +0100 |
hoelzl |
add L'Hôpital's rule
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:05 +0100 |
hoelzl |
add filterlim rules for exp and ln to infinity
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:04 +0100 |
hoelzl |
add filterlim rules for inverse and at_infinity
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:02 +0100 |
hoelzl |
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:01 +0100 |
hoelzl |
add filterlim rules for unary minus and inverse
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:18:59 +0100 |
hoelzl |
rename filter_lim to filterlim to be consistent with filtermap
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 19:31:11 +0100 |
hoelzl |
introduce filter_lim as a generatlization of tendsto
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:34:43 +0100 |
noschinl |
use eventually_elim method
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:28:10 +0100 |
noschinl |
add eventually_elim method
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 15:55:39 +0100 |
noschinl |
add lemmas about limits
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 10:52:08 -0700 |
huffman |
add lemmas within_empty and tendsto_bot;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 07:51:55 -0700 |
huffman |
convert to Isar-style proof
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 20:56:49 -0700 |
huffman |
move class perfect_space into RealVector.thy;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 06:34:51 -0700 |
huffman |
redefine constant 'trivial_limit' as an abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 11:39:09 -0700 |
huffman |
add lemma tendsto_compose_eventually; use it to shorten some proofs
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 11:06:39 -0700 |
huffman |
add lemma metric_tendsto_imp_tendsto
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 16:48:05 -0700 |
huffman |
add lemma tendsto_compose
|
file |
diff |
annotate
|
| Sun, 14 Aug 2011 10:47:47 -0700 |
huffman |
locale-ize some constant definitions, so complete_space can inherit from metric_space
|
file |
diff |
annotate
|
| Sun, 14 Aug 2011 10:25:43 -0700 |
huffman |
generalize constant 'lim' and limit uniqueness theorems to class t2_space
|
file |
diff |
annotate
|
| Sun, 14 Aug 2011 08:45:38 -0700 |
huffman |
consistently use variable name 'F' for filters
|
file |
diff |
annotate
|
| Sun, 14 Aug 2011 07:54:24 -0700 |
huffman |
generalize lemmas about LIM and LIMSEQ to tendsto
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:26:53 -0700 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 16:57:37 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:35 +0100 |
hoelzl |
generalize infinite sums
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 10 May 2010 21:33:48 -0700 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 04 May 2010 13:08:56 -0700 |
huffman |
generalize types of LIMSEQ and LIM; generalize many lemmas
|
file |
diff |
annotate
|
| Mon, 03 May 2010 18:40:48 -0700 |
huffman |
add lemmas eventually_nhds_metric and tendsto_mono
|
file |
diff |
annotate
|
| Mon, 03 May 2010 17:39:46 -0700 |
huffman |
remove unneeded premise
|
file |
diff |
annotate
|
| Mon, 03 May 2010 17:13:37 -0700 |
huffman |
add constants netmap and nhds
|
file |
diff |
annotate
|
| Sat, 01 May 2010 11:46:47 -0700 |
huffman |
complete_lattice instance for net type
|
file |
diff |
annotate
|
| Sat, 01 May 2010 09:43:40 -0700 |
huffman |
swap ordering on nets, so x <= y means 'x is finer than y'
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 20:48:19 -0700 |
huffman |
define finer-than ordering on net type; move some theorems into Limits.thy
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 11:58:39 -0700 |
huffman |
define nets directly as filters, instead of as filter bases
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 15:46:21 -0700 |
huffman |
add lemma tendsto_setsum
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 11:51:12 -0700 |
huffman |
theorem attribute [tendsto_intros]
|
file |
diff |
annotate
|
| Sun, 07 Jun 2009 17:59:54 -0700 |
huffman |
replace 'topo' with 'open'; add extra type constraint for 'open'
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 09:11:12 -0700 |
huffman |
generalize tendsto to class topological_space
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 15:59:20 -0700 |
huffman |
put syntax for tendsto in Limits.thy; rename variables
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 17:24:09 -0700 |
huffman |
generalize type of 'at' to topological_space; generalize some lemmas
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 17:03:22 -0700 |
huffman |
replace filters with filter bases
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 16:27:54 -0700 |
huffman |
declare Bfun_def [code del]
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 10:56:31 -0700 |
huffman |
simp del -> code del
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 10:36:42 -0700 |
huffman |
limits of inverse using filters
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 07:57:37 -0700 |
huffman |
add [code del] declarations
|
file |
diff |
annotate
|
| Sun, 31 May 2009 21:59:33 -0700 |
huffman |
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
|
file |
diff |
annotate
|