de-applying

more de-applying

de-applying, etc.

de-applying

Incorporating new/strengthened proofs from Library and AFP entries

tidying and reorganisation around Cauchy Integral Theorem

type class generalisations; some work on infinite products

tuned proofs and generalized some lemmas about limits

--HG--
extra : transplant_source : 5L%7B%84%AC%23%07%FCx%BD.%0C%24%7EY%1A%AB%9C%1B%B7

Added some simple facts about limits

Unified the order of zeros and poles; improved reasoning around non-essential singularites

--HG--
extra : amend_source : 528e99138923389ffcb3b2021c959a3c9f20de52

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

lots of new material, ultimately related to measure theory

ran isabelle update_op on all sources

moved in some material from Euler-MacLaurin

more symbols;

Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems

new material about connectedness, etc.

Various lemmas for HOL-Analysis

Replaced subseq with strict_mono

Simplification of some proofs. Also key lemmas using !! rather than ! in premises

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas

Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

more new material

more from moretop.ml

setprod -> prod

setsum -> sum

new material connected with HOL Light measure theory, plus more rationalisation

tuned proofs;

More analysis lemmas

numerical bounds on pi

unused (see 1e9e68247ad1);

misc tuning and modernization;

new results about topology

approximation, derivative, and continuity of floor and ceiling

reduce isUCont to uniformly_continuous_on

introduced class topological_group between topological_monoid and real_normed_vector

eliminated old 'def';
tuned comments;

New and revised material for (multivariate) analysis

more canonical names

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

instantiate topologies for nat, int and enat

--HG--
extra : rebase_source : 2320da44d4913f441c671ef425945fac6d4381c9

add type class for topological monoids

--HG--
extra : rebase_source : bedca3d32972c3f447e37ac5aac3de5ac763b94b

add uniform spaces

revisions to limits and derivatives, plus new lemmas

more symbols;

more symbols;

more symbols;

transfer rule for bounded_linear of blinfun

sorted out eventually_mono

Cauchy's integral formula for circles. Starting to fix eventually_mono.

isabelle update_cartouches -c -t;

New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.

Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

Rounding function, uniform limits, cotangent, binomial identities

added many small lemmas about setsum/setprod/powr/...

tuned proofs -- less legacy;

eliminated \<Colon>;

New material and fixes related to the forthcoming Stone-Weierstrass development

isabelle update_cartouches;

generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal

generalized tends over powr; added DERIV rule for powr

--HG--
extra : rebase_source : e5262f95063d694a1b08a65810ad2c515d8583a6

New material, mostly about limits. Consolidation.

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

given up separate type classes demanding `inverse 0 = 0`

The function frac. Various lemmas about limits, series, the exp function, etc.

modernized header uniformly as section;

add tendsto_const and tendsto_ident_at as simp and intro rules

--HG--
extra : rebase_source : 22eac3c1e90ec123e3d2513334c670b5eb22d7e7

reduced name variants for assoc and commute on plus and mult

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

filters are easier to define with INF on filters.

--HG--
extra : rebase_source : 5626307315d6be224d16a97b9160690f09c8e0d4

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

made divide_pos_pos a simp rule

made mult_nonneg_nonneg a simp rule

--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36

extend continuous_intros; remove continuous_on_intros and isCont_intros

new theorem about zero limits

add limits of power at top and bot

renamed 'nat_{case,rec}' to '{case,rec}_nat'

prefer more canonical names for lemmas on min/max

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

--HG--
rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

tuned proofs

tuned proofs -- less guessing;

tuned headers;

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

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces

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

move SEQ.thy and Lim.thy to Limits.thy

rename RealVector.thy to Real_Vector_Spaces.thy

--HG--
rename : src/HOL/RealVector.thy => src/HOL/Real_Vector_Spaces.thy

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)

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

move metric_space to its own theory

move topological_space to its own theory

add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->

move auxiliary lemmas from Library/Extended_Reals to HOL image

replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules

introduce order topology

move eventually_Ball_finite to Limits

--HG--
extra : rebase_source : 0d150f5a1d1c24afa1c8eef2d6d8ccc1b282306b

add exponential and uniform distributions

prove tendsto_power_div_exp_0
* * *
missing rename

--HG--
extra : rebase_source : 2809e8af73b029406c9ce85b75b90c6fbf6cada9

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

--HG--
extra : rebase_source : 327fe91b9d9d244286b9a29c61e2f5fe56c9e295

use filterlim in Lim and SEQ; tuned proofs

conversion rules for at, at_left and at_right; applied to l'Hopital's rules.

add L'Hôpital's rule

add filterlim rules for exp and ln to infinity

add filterlim rules for inverse and at_infinity

add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image

add filterlim rules for unary minus and inverse

rename filter_lim to filterlim to be consistent with filtermap

introduce filter_lim as a generatlization of tendsto

discontinued obsolete typedef (open) syntax;

more standard method setup;

use eventually_elim method

add eventually_elim method

add lemmas about limits

tuned Named_Thms: proper binding;

add lemmas within_empty and tendsto_bot;
declare within_UNIV [simp];
tuned some proofs;

convert to Isar-style proof

move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;

discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

redefine constant 'trivial_limit' as an abbreviation

remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

add lemma tendsto_compose_eventually; use it to shorten some proofs

add lemma metric_tendsto_imp_tendsto

add lemma tendsto_compose

locale-ize some constant definitions, so complete_space can inherit from metric_space

--HG--
extra : transplant_source : %A7%2BZv%3BkQK%CC%2A%90%83%9EC%8F%8B%04%A1%EAj

generalize constant 'lim' and limit uniqueness theorems to class t2_space

--HG--
extra : transplant_source : %8B%8E%F2%E2%F4Gx%16%A3%9BK%C4%F2%80%0F%AB%F1%FD%B0%EC

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

rename type 'a net to 'a filter, following standard mathematical terminology

remove duplicate lemmas

generalize infinite sums

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

dropped superfluous [code del]s

minimize imports

generalize types of LIMSEQ and LIM; generalize many lemmas

add lemmas eventually_nhds_metric and tendsto_mono

remove unneeded premise

add constants netmap and nhds

complete_lattice instance for net type

swap ordering on nets, so x <= y means 'x is finer than y'

define finer-than ordering on net type; move some theorems into Limits.thy

define nets directly as filters, instead of as filter bases

renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;

add lemma tendsto_setsum

theorem attribute [tendsto_intros]

replace 'topo' with 'open'; add extra type constraint for 'open'

generalize tendsto to class topological_space

put syntax for tendsto in Limits.thy; rename variables

generalize type of 'at' to topological_space; generalize some lemmas

replace filters with filter bases

declare Bfun_def [code del]

simp del -> code del

limits of inverse using filters

add [code del] declarations

new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters