Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-22 12:52 cb618e01

View on Github →

feat(analysis/analytic): a continuous linear map defines an analytic function (#5840) Also add convenience lemmas with conclusion radius = ⊤.

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem formal_multilinear_series.radius_eq_top_of_eventually_eq_zero

added theorem formal_multilinear_series.radius_eq_top_of_forall_image_add_eq_zero

added theorem formal_multilinear_series.radius_eq_top_of_forall_nnreal_is_O

Created src/analysis/analytic/linear.lean

added def continuous_linear_map.fpower_series

added theorem continuous_linear_map.fpower_series_apply_add_two

added theorem continuous_linear_map.fpower_series_radius

Modified src/data/real/ennreal.lean

added theorem ennreal.eq_top_of_forall_nnreal_le