Commit 2020-04-26 09:29 11ccc1b5

View on Github →

feat(analysis/calculus/deriv): define has_strict_deriv_at (#2524) Also make more proofs explicitly use their has_fderiv* counterparts and mark some lemmas in fderiv as protected.

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem continuous_linear_map.deriv

added theorem continuous_linear_map.deriv_within

added theorem continuous_linear_map.has_deriv_at

added theorem continuous_linear_map.has_deriv_at_filter

added theorem continuous_linear_map.has_deriv_within_at

added theorem continuous_linear_map.has_strict_deriv_at

deleted theorem has_deriv_at_inv_one

added theorem has_fderiv_at.has_deriv_at

added theorem has_fderiv_at_filter.has_deriv_at_filter

added theorem has_fderiv_within_at.has_deriv_within_at

added theorem has_strict_deriv_at.add

added theorem has_strict_deriv_at.comp

added theorem has_strict_deriv_at.has_deriv_at

added theorem has_strict_deriv_at.mul

added theorem has_strict_deriv_at.neg

added theorem has_strict_deriv_at.scomp

added theorem has_strict_deriv_at.smul

added theorem has_strict_deriv_at.sub

added def has_strict_deriv_at

added theorem has_strict_deriv_at_const

added theorem has_strict_deriv_at_fpow

added theorem has_strict_deriv_at_id

added theorem has_strict_deriv_at_inv

added theorem has_strict_deriv_at_pow

added theorem has_strict_fderiv_at.has_strict_deriv_at

added theorem has_strict_fderiv_at_iff_has_strict_deriv_at

deleted theorem is_linear_map.deriv

deleted theorem is_linear_map.deriv_within

deleted theorem is_linear_map.differentiable

deleted theorem is_linear_map.differentiable_at

deleted theorem is_linear_map.differentiable_on

deleted theorem is_linear_map.differentiable_within_at

deleted theorem is_linear_map.has_deriv_at

deleted theorem is_linear_map.has_deriv_at_filter

deleted theorem is_linear_map.has_deriv_within_at

added theorem linear_map.deriv

added theorem linear_map.deriv_within

added theorem linear_map.has_deriv_at

added theorem linear_map.has_deriv_at_filter

added theorem linear_map.has_deriv_within_at

added theorem linear_map.has_strict_deriv_at

Modified src/analysis/calculus/fderiv.lean

deleted theorem differentiable.fst

deleted theorem differentiable.snd

deleted theorem differentiable_at.fst

deleted theorem differentiable_at.prod_map

deleted theorem differentiable_at.snd

deleted theorem differentiable_on.fst

deleted theorem differentiable_on.snd

deleted theorem differentiable_within_at.fst

deleted theorem differentiable_within_at.snd

deleted theorem has_fderiv_at.fst

deleted theorem has_fderiv_at.prod_map

deleted theorem has_fderiv_at.snd

deleted theorem has_fderiv_at_filter.fst

deleted theorem has_fderiv_at_filter.snd

deleted theorem has_fderiv_within_at.fst

deleted theorem has_fderiv_within_at.snd

added theorem has_strict_fderiv_at.congr_of_mem_sets

deleted theorem has_strict_fderiv_at.fst

deleted theorem has_strict_fderiv_at.prod_map

Modified src/analysis/normed_space/operator_norm.lean

added def linear_map.to_continuous_linear_map₁

added theorem linear_map.to_continuous_linear_map₁_apply

added theorem linear_map.to_continuous_linear_map₁_coe

Modified src/linear_algebra/basic.lean