Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-31 05:47 66f30901

View on Github →

feat(analysis/analytic): first take on analytic functions (#2199)

analytic: first definitions
docstrings
cleanup
Update src/analysis/analytic/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
comment on polydisk of convergence
coefficient at 0
protect sum
rename with_top.dense_coe

Estimated changes

Created src/analysis/analytic/basic.lean

added theorem analytic_at.add

added theorem analytic_at.continuous_at

added theorem analytic_at.neg

added theorem analytic_at.sub

added def analytic_at

added theorem formal_multilinear_series.bound_of_lt_radius

added theorem formal_multilinear_series.continuous_on

added theorem formal_multilinear_series.geometric_bound_of_lt_radius

added theorem formal_multilinear_series.has_fpower_series_on_ball

added theorem formal_multilinear_series.le_radius_of_bound

added theorem formal_multilinear_series.min_radius_le_radius_add

added def formal_multilinear_series.partial_sum

added theorem formal_multilinear_series.partial_sum_continuous

added def formal_multilinear_series.radius

added theorem formal_multilinear_series.radius_neg

added theorem has_fpower_series_at.add

added theorem has_fpower_series_at.analytic_at

added theorem has_fpower_series_at.coeff_zero

added theorem has_fpower_series_at.continuous_at

added theorem has_fpower_series_at.neg

added theorem has_fpower_series_at.radius_pos

added theorem has_fpower_series_at.sub

added def has_fpower_series_at

added theorem has_fpower_series_on_ball.add

added theorem has_fpower_series_on_ball.analytic_at

added theorem has_fpower_series_on_ball.coeff_zero

added theorem has_fpower_series_on_ball.continuous_on

added theorem has_fpower_series_on_ball.has_fpower_series_at

added theorem has_fpower_series_on_ball.mono

added theorem has_fpower_series_on_ball.neg

added theorem has_fpower_series_on_ball.radius_pos

added theorem has_fpower_series_on_ball.sub

added theorem has_fpower_series_on_ball.sum

added theorem has_fpower_series_on_ball.uniform_limit

added structure has_fpower_series_on_ball

Modified src/data/real/ennreal.lean

added theorem ennreal.lt_iff_exists_nnreal_btwn

Modified src/data/set/finite.lean

added theorem finset.bdd_above

added theorem finset.bdd_below

Modified src/order/bounded_lattice.lean

deleted theorem with_top.dense_coe

added theorem with_top.lt_iff_exists_coe_btwn

Modified src/topology/metric_space/emetric_space.lean