Commit 2022-09-03 22:00 a6ca2e8f

View on Github →

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros (#15908) Local version: an analytic function is either locally zero, or nonzero in a punctured neighborhood.

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem has_fpower_series_at.congr

added theorem has_fpower_series_at.eq_formal_multilinear_series_of_eventually

added theorem has_fpower_series_at.eq_zero_of_eventually

added theorem has_fpower_series_at.eventually_eq_zero

added theorem has_fpower_series_at.eventually_has_sum

added theorem has_fpower_series_at.eventually_has_sum_sub

added theorem has_fpower_series_at_iff'

added theorem has_fpower_series_at_iff

added theorem has_fpower_series_on_ball.eventually_eq_zero

added theorem has_fpower_series_on_ball.eventually_has_sum

added theorem has_fpower_series_on_ball.eventually_has_sum_sub

Created src/analysis/analytic/isolated_zeros.lean

added theorem analytic_at.eventually_eq_zero_or_eventually_ne_zero

added theorem has_fpower_series_at.eq_pow_order_mul_iterate_dslope

added theorem has_fpower_series_at.has_fpower_series_dslope_fslope

added theorem has_fpower_series_at.has_fpower_series_iterate_dslope_fslope

added theorem has_fpower_series_at.iterate_dslope_fslope_ne_zero

added theorem has_fpower_series_at.locally_ne_zero

added theorem has_fpower_series_at.locally_zero_iff

added theorem has_sum.exists_has_sum_smul_of_apply_eq_zero

added theorem has_sum.has_sum_at_zero

Modified src/analysis/calculus/formal_multilinear_series.lean

added theorem formal_multilinear_series.apply_eq_pow_smul_coeff

added theorem formal_multilinear_series.apply_eq_prod_smul_coeff

added theorem formal_multilinear_series.apply_eq_zero_of_lt_order

added theorem formal_multilinear_series.apply_order_ne_zero'

added theorem formal_multilinear_series.apply_order_ne_zero

added def formal_multilinear_series.coeff

added theorem formal_multilinear_series.coeff_eq_zero

added theorem formal_multilinear_series.coeff_fslope

added theorem formal_multilinear_series.coeff_iterate_fslope

added theorem formal_multilinear_series.mk_pi_field_coeff_eq

added theorem formal_multilinear_series.ne_zero_of_order_ne_zero

added theorem formal_multilinear_series.norm_apply_eq_norm_coef

added theorem formal_multilinear_series.order_eq_find'

added theorem formal_multilinear_series.order_eq_find

added theorem formal_multilinear_series.order_eq_zero_iff'

added theorem formal_multilinear_series.order_eq_zero_iff

added theorem formal_multilinear_series.order_zero

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.mk_pi_field_eq_iff

added theorem continuous_multilinear_map.mk_pi_field_eq_zero_iff

added theorem continuous_multilinear_map.mk_pi_field_zero

Modified src/linear_algebra/multilinear/basic.lean

added theorem multilinear_map.mk_pi_ring_eq_iff

added theorem multilinear_map.mk_pi_ring_eq_zero_iff

added theorem multilinear_map.mk_pi_ring_zero

Modified src/topology/algebra/module/multilinear.lean

added theorem continuous_multilinear_map.ext_iff

Modified src/topology/separation.lean

added theorem continuous_at.eventually_ne

added theorem filter.tendsto.eventually_ne