Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-27 19:40 3bce8d80

View on Github →

chore(analysis/calculus/deriv): split file (#19113)

  • Split analysis.calculus.deriv into smaller files.
  • Add copyright headers and (stubs of) module docstrings.
  • Change proofs of derivatives of pow and polynomial so that analysis.calculus.deriv.pow does not depend on polynomials.

Estimated changes

deleted theorem deriv.comp
deleted theorem deriv.neg'
deleted theorem deriv.neg
deleted theorem deriv.scomp
deleted def deriv
deleted theorem deriv_add
deleted theorem deriv_add_const'
deleted theorem deriv_add_const
deleted theorem deriv_clm_apply
deleted theorem deriv_clm_comp
deleted theorem deriv_const'
deleted theorem deriv_const
deleted theorem deriv_const_add'
deleted theorem deriv_const_add
deleted theorem deriv_const_mul
deleted theorem deriv_const_mul_field'
deleted theorem deriv_const_mul_field
deleted theorem deriv_const_smul
deleted theorem deriv_const_sub
deleted theorem deriv_div
deleted theorem deriv_div_const
deleted theorem deriv_eq
deleted theorem deriv_fderiv
deleted theorem deriv_id''
deleted theorem deriv_id'
deleted theorem deriv_id
deleted theorem deriv_inv''
deleted theorem deriv_inv'
deleted theorem deriv_inv
deleted theorem deriv_mem_iff
deleted theorem deriv_mul
deleted theorem deriv_mul_const
deleted theorem deriv_mul_const_field'
deleted theorem deriv_mul_const_field
deleted theorem deriv_neg''
deleted theorem deriv_neg'
deleted theorem deriv_neg
deleted theorem deriv_pi
deleted theorem deriv_pow''
deleted theorem deriv_pow'
deleted theorem deriv_pow
deleted theorem deriv_smul
deleted theorem deriv_smul_const
deleted theorem deriv_sub
deleted theorem deriv_sub_const
deleted theorem deriv_sum
deleted theorem deriv_within.comp
deleted theorem deriv_within.neg
deleted theorem deriv_within.scomp
deleted def deriv_within
deleted theorem deriv_within_Ioi_eq_Ici
deleted theorem deriv_within_add
deleted theorem deriv_within_add_const
deleted theorem deriv_within_clm_apply
deleted theorem deriv_within_clm_comp
deleted theorem deriv_within_congr
deleted theorem deriv_within_congr_set'
deleted theorem deriv_within_congr_set
deleted theorem deriv_within_const
deleted theorem deriv_within_const_add
deleted theorem deriv_within_const_mul
deleted theorem deriv_within_const_smul
deleted theorem deriv_within_const_sub
deleted theorem deriv_within_div
deleted theorem deriv_within_div_const
deleted theorem deriv_within_id
deleted theorem deriv_within_inter
deleted theorem deriv_within_inv'
deleted theorem deriv_within_inv
deleted theorem deriv_within_mem_iff
deleted theorem deriv_within_mul
deleted theorem deriv_within_mul_const
deleted theorem deriv_within_neg
deleted theorem deriv_within_of_mem
deleted theorem deriv_within_of_open
deleted theorem deriv_within_pi
deleted theorem deriv_within_pow'
deleted theorem deriv_within_pow
deleted theorem deriv_within_smul
deleted theorem deriv_within_smul_const
deleted theorem deriv_within_sub
deleted theorem deriv_within_sub_const
deleted theorem deriv_within_subset
deleted theorem deriv_within_sum
deleted theorem deriv_within_univ
deleted theorem deriv_within_zpow
deleted theorem deriv_zpow'
deleted theorem deriv_zpow
deleted theorem differentiable.div
deleted theorem differentiable.div_const
deleted theorem differentiable.inv
deleted theorem differentiable.zpow
deleted theorem differentiable_at.div
deleted theorem differentiable_at.inv
deleted theorem differentiable_at.zpow
deleted theorem differentiable_at_inv
deleted theorem differentiable_at_pow
deleted theorem differentiable_at_zpow
deleted theorem differentiable_neg
deleted theorem differentiable_on.div
deleted theorem differentiable_on.inv
deleted theorem differentiable_on.zpow
deleted theorem differentiable_on_inv
deleted theorem differentiable_on_neg
deleted theorem differentiable_on_pow
deleted theorem differentiable_on_zpow
deleted theorem differentiable_pow
deleted theorem fderiv.comp_deriv
deleted theorem fderiv_deriv
deleted theorem fderiv_inv
deleted theorem fderiv_within_inv
deleted theorem has_compact_support.deriv
deleted theorem has_deriv_at.add
deleted theorem has_deriv_at.add_const
deleted theorem has_deriv_at.clm_apply
deleted theorem has_deriv_at.clm_comp
deleted theorem has_deriv_at.comp
deleted theorem has_deriv_at.const_add
deleted theorem has_deriv_at.const_mul
deleted theorem has_deriv_at.const_smul
deleted theorem has_deriv_at.const_sub
deleted theorem has_deriv_at.deriv
deleted theorem has_deriv_at.div
deleted theorem has_deriv_at.div_const
deleted theorem has_deriv_at.inv
deleted theorem has_deriv_at.mul
deleted theorem has_deriv_at.mul_const
deleted theorem has_deriv_at.neg
deleted theorem has_deriv_at.pow
deleted theorem has_deriv_at.prod
deleted theorem has_deriv_at.scomp
deleted theorem has_deriv_at.smul
deleted theorem has_deriv_at.smul_const
deleted theorem has_deriv_at.sub
deleted theorem has_deriv_at.sub_const
deleted theorem has_deriv_at.sum
deleted theorem has_deriv_at.unique
deleted def has_deriv_at
deleted theorem has_deriv_at_const
deleted theorem has_deriv_at_deriv_iff
deleted theorem has_deriv_at_filter.add
deleted theorem has_deriv_at_filter.comp
deleted theorem has_deriv_at_filter.mono
deleted theorem has_deriv_at_filter.neg
deleted theorem has_deriv_at_filter.prod
deleted theorem has_deriv_at_filter.scomp
deleted theorem has_deriv_at_filter.sub
deleted theorem has_deriv_at_filter.sum
deleted def has_deriv_at_filter
deleted theorem has_deriv_at_filter_const
deleted theorem has_deriv_at_filter_id
deleted theorem has_deriv_at_filter_neg
deleted theorem has_deriv_at_filter_pi
deleted theorem has_deriv_at_id'
deleted theorem has_deriv_at_id
deleted theorem has_deriv_at_iff_is_o
deleted theorem has_deriv_at_iff_tendsto
deleted theorem has_deriv_at_inv
deleted theorem has_deriv_at_mul_const
deleted theorem has_deriv_at_neg'
deleted theorem has_deriv_at_neg
deleted theorem has_deriv_at_pi
deleted theorem has_deriv_at_pow
deleted theorem has_deriv_at_zpow
deleted theorem has_deriv_within_at.add
deleted theorem has_deriv_within_at.comp
deleted theorem has_deriv_within_at.congr
deleted theorem has_deriv_within_at.div
deleted theorem has_deriv_within_at.inv
deleted theorem has_deriv_within_at.mono
deleted theorem has_deriv_within_at.mul
deleted theorem has_deriv_within_at.neg
deleted theorem has_deriv_within_at.pow
deleted theorem has_deriv_within_at.prod
deleted theorem has_deriv_within_at.scomp
deleted theorem has_deriv_within_at.smul
deleted theorem has_deriv_within_at.sub
deleted theorem has_deriv_within_at.sum
deleted theorem has_deriv_within_at.union
deleted def has_deriv_within_at
deleted theorem has_deriv_within_at_const
deleted theorem has_deriv_within_at_id
deleted theorem has_deriv_within_at_inter
deleted theorem has_deriv_within_at_inv
deleted theorem has_deriv_within_at_neg
deleted theorem has_deriv_within_at_pi
deleted theorem has_deriv_within_at_pow
deleted theorem has_deriv_within_at_univ
deleted theorem has_deriv_within_at_zpow
deleted theorem has_fderiv_at_inv
deleted theorem has_fderiv_within_at_inv
deleted theorem has_strict_deriv_at.add
deleted theorem has_strict_deriv_at.comp
deleted theorem has_strict_deriv_at.div
deleted theorem has_strict_deriv_at.mul
deleted theorem has_strict_deriv_at.neg
deleted theorem has_strict_deriv_at.prod
deleted theorem has_strict_deriv_at.scomp
deleted theorem has_strict_deriv_at.smul
deleted theorem has_strict_deriv_at.sub
deleted theorem has_strict_deriv_at.sum
deleted def has_strict_deriv_at
deleted theorem has_strict_deriv_at_const
deleted theorem has_strict_deriv_at_id
deleted theorem has_strict_deriv_at_inv
deleted theorem has_strict_deriv_at_neg
deleted theorem has_strict_deriv_at_pi
deleted theorem has_strict_deriv_at_pow
deleted theorem has_strict_deriv_at_zpow
deleted theorem iter_deriv_inv'
deleted theorem iter_deriv_inv
deleted theorem iter_deriv_pow'
deleted theorem iter_deriv_pow
deleted theorem iter_deriv_zpow'
deleted theorem iter_deriv_zpow
deleted theorem support_deriv_subset
added theorem deriv.neg'
added theorem deriv.neg
added theorem deriv_add
added theorem deriv_add_const'
added theorem deriv_add_const
added theorem deriv_const_add'
added theorem deriv_const_add
added theorem deriv_const_sub
added theorem deriv_neg''
added theorem deriv_neg'
added theorem deriv_neg
added theorem deriv_sub
added theorem deriv_sub_const
added theorem deriv_sum
added theorem deriv_within.neg
added theorem deriv_within_add
added theorem deriv_within_add_const
added theorem deriv_within_const_add
added theorem deriv_within_const_sub
added theorem deriv_within_neg
added theorem deriv_within_sub
added theorem deriv_within_sub_const
added theorem deriv_within_sum
added theorem differentiable_neg
added theorem differentiable_on_neg
added theorem has_deriv_at.add
added theorem has_deriv_at.add_const
added theorem has_deriv_at.const_add
added theorem has_deriv_at.const_sub
added theorem has_deriv_at.neg
added theorem has_deriv_at.sub
added theorem has_deriv_at.sub_const
added theorem has_deriv_at.sum
added theorem has_deriv_at_neg'
added theorem has_deriv_at_neg
added def deriv
added theorem deriv_const'
added theorem deriv_const
added theorem deriv_eq
added theorem deriv_fderiv
added theorem deriv_id''
added theorem deriv_id'
added theorem deriv_id
added theorem deriv_mem_iff
added def deriv_within
added theorem deriv_within_congr
added theorem deriv_within_congr_set
added theorem deriv_within_const
added theorem deriv_within_id
added theorem deriv_within_inter
added theorem deriv_within_mem_iff
added theorem deriv_within_of_mem
added theorem deriv_within_of_open
added theorem deriv_within_subset
added theorem deriv_within_univ
added theorem fderiv_deriv
added theorem has_deriv_at.deriv
added theorem has_deriv_at.unique
added def has_deriv_at
added theorem has_deriv_at_const
added theorem has_deriv_at_deriv_iff
added theorem has_deriv_at_filter_id
added theorem has_deriv_at_id'
added theorem has_deriv_at_id
added theorem has_deriv_at_iff_is_o
added theorem has_deriv_within_at_id
added theorem has_strict_deriv_at_id
added theorem deriv.comp
added theorem deriv.scomp
added theorem deriv_within.comp
added theorem deriv_within.scomp
added theorem fderiv.comp_deriv
added theorem has_deriv_at.comp
added theorem has_deriv_at.scomp
added theorem deriv_div
added theorem deriv_inv''
added theorem deriv_inv'
added theorem deriv_inv
added theorem deriv_within_div
added theorem deriv_within_inv'
added theorem deriv_within_inv
added theorem differentiable.div
added theorem differentiable.inv
added theorem differentiable_at.div
added theorem differentiable_at.inv
added theorem differentiable_at_inv
added theorem differentiable_on.div
added theorem differentiable_on.inv
added theorem differentiable_on_inv
added theorem fderiv_inv
added theorem fderiv_within_inv
added theorem has_deriv_at.div
added theorem has_deriv_at.inv
added theorem has_deriv_at_inv
added theorem has_fderiv_at_inv
added theorem deriv_clm_apply
added theorem deriv_clm_comp
added theorem deriv_const_mul
added theorem deriv_const_mul_field'
added theorem deriv_const_mul_field
added theorem deriv_const_smul
added theorem deriv_div_const
added theorem deriv_mul
added theorem deriv_mul_const
added theorem deriv_mul_const_field'
added theorem deriv_mul_const_field
added theorem deriv_smul
added theorem deriv_smul_const
added theorem deriv_within_clm_apply
added theorem deriv_within_clm_comp
added theorem deriv_within_const_mul
added theorem deriv_within_div_const
added theorem deriv_within_mul
added theorem deriv_within_mul_const
added theorem deriv_within_smul
added theorem has_deriv_at.clm_apply
added theorem has_deriv_at.clm_comp
added theorem has_deriv_at.const_mul
added theorem has_deriv_at.div_const
added theorem has_deriv_at.mul
added theorem has_deriv_at.mul_const
added theorem has_deriv_at.smul
added theorem has_deriv_at_mul_const
added theorem deriv_pow''
added theorem deriv_pow'
added theorem deriv_pow
added theorem deriv_within_pow'
added theorem deriv_within_pow
added theorem differentiable_at_pow
added theorem differentiable_on_pow
added theorem differentiable_pow
added theorem has_deriv_at.pow
added theorem has_deriv_at_pow
added theorem deriv_pi
added theorem deriv_within_pi
added theorem has_deriv_at.prod
added theorem has_deriv_at_filter_pi
added theorem has_deriv_at_pi
added theorem has_deriv_within_at_pi
added theorem has_strict_deriv_at_pi
added theorem support_deriv_subset
added theorem deriv_within_zpow
added theorem deriv_zpow'
added theorem deriv_zpow
added theorem differentiable.zpow
added theorem differentiable_at.zpow
added theorem differentiable_at_zpow
added theorem differentiable_on.zpow
added theorem differentiable_on_zpow
added theorem has_deriv_at_zpow
added theorem iter_deriv_inv'
added theorem iter_deriv_inv
added theorem iter_deriv_pow'
added theorem iter_deriv_pow
added theorem iter_deriv_zpow'
added theorem iter_deriv_zpow