Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-23 22:13 439ac4e9

View on Github →

feat(analysis/calculus/local_extr): Fermat's Theorem, Rolle's Theorem, Lagrange's MVT, Cauchy's MVT (#1807)

  • feat(analysis/calculus/local_extr): Rolle's Theorem, Lagrange's MVT, Cauchy's MVT
  • feat(order/filter/extr,topology/algebra/local_extr): local min/max points This commit contains facts that do not require smooth structure on the domain.
  • Rewrite: introduce is_min_filter, pos_tangent_cone_at.
  • Fix compile, move code around
  • Drop a TODO, add some docs
  • Fix compile
  • Fix a typo
  • Fix #lint error
  • Add some docstrings
  • Add some missing lemmas
  • Use differentiable_on
  • Add/rewrite file-level docs, rename some lemmas.
  • Update src/analysis/calculus/local_extr.lean
  • Update src/order/filter/extr.lean
  • Fix a docstring, add Wiki links
  • Add refs and tags
  • File docstring: provide Lean names of the main lemmas.
  • Update src/analysis/calculus/local_extr.lean
  • Update src/analysis/calculus/local_extr.lean

Estimated changes

added theorem exists_Ioo_extr_on_Icc
added theorem exists_deriv_eq_zero
added theorem exists_local_extr_Ioo
added theorem exists_deriv_eq_slope
added theorem is_extr_filter.neg
added def is_extr_filter
added theorem is_extr_filter_const
added theorem is_extr_on.comp_mono
added theorem is_extr_on.elim
added theorem is_extr_on.inter
added theorem is_extr_on.neg
added theorem is_extr_on.on_preimage
added theorem is_extr_on.on_subset
added def is_extr_on
added theorem is_extr_on_const
added theorem is_extr_on_dual_iff
added theorem is_max_filter.add
added theorem is_max_filter.inf
added theorem is_max_filter.is_extr
added theorem is_max_filter.max
added theorem is_max_filter.min
added theorem is_max_filter.neg
added theorem is_max_filter.sub
added theorem is_max_filter.sup
added def is_max_filter
added theorem is_max_filter_const
added theorem is_max_filter_dual_iff
added theorem is_max_on.add
added theorem is_max_on.bicomp_mono
added theorem is_max_on.comp_mono
added theorem is_max_on.inf
added theorem is_max_on.inter
added theorem is_max_on.is_extr
added theorem is_max_on.max
added theorem is_max_on.min
added theorem is_max_on.neg
added theorem is_max_on.on_preimage
added theorem is_max_on.on_subset
added theorem is_max_on.sub
added theorem is_max_on.sup
added def is_max_on
added theorem is_max_on_const
added theorem is_max_on_dual_iff
added theorem is_max_on_iff
added theorem is_max_on_univ_iff
added theorem is_min_filter.add
added theorem is_min_filter.inf
added theorem is_min_filter.is_extr
added theorem is_min_filter.max
added theorem is_min_filter.min
added theorem is_min_filter.neg
added theorem is_min_filter.sub
added theorem is_min_filter.sup
added def is_min_filter
added theorem is_min_filter_const
added theorem is_min_filter_dual_iff
added theorem is_min_on.add
added theorem is_min_on.bicomp_mono
added theorem is_min_on.comp_mono
added theorem is_min_on.inf
added theorem is_min_on.inter
added theorem is_min_on.is_extr
added theorem is_min_on.max
added theorem is_min_on.min
added theorem is_min_on.neg
added theorem is_min_on.on_preimage
added theorem is_min_on.on_subset
added theorem is_min_on.sub
added theorem is_min_on.sup
added def is_min_on
added theorem is_min_on_const
added theorem is_min_on_dual_iff
added theorem is_min_on_iff
added theorem is_min_on_univ_iff
added theorem is_extr_on.localize
added theorem is_local_extr.elim
added theorem is_local_extr.neg
added theorem is_local_extr.on
added def is_local_extr
added theorem is_local_extr_const
added theorem is_local_extr_on.elim
added theorem is_local_extr_on.inter
added theorem is_local_extr_on.neg
added def is_local_extr_on
added theorem is_local_extr_on_const
added theorem is_local_max.add
added theorem is_local_max.comp_mono
added theorem is_local_max.inf
added theorem is_local_max.max
added theorem is_local_max.min
added theorem is_local_max.neg
added theorem is_local_max.on
added theorem is_local_max.sub
added theorem is_local_max.sup
added def is_local_max
added theorem is_local_max_const
added theorem is_local_max_on.add
added theorem is_local_max_on.inf
added theorem is_local_max_on.inter
added theorem is_local_max_on.max
added theorem is_local_max_on.min
added theorem is_local_max_on.neg
added theorem is_local_max_on.sub
added theorem is_local_max_on.sup
added def is_local_max_on
added theorem is_local_max_on_const
added theorem is_local_min.add
added theorem is_local_min.comp_mono
added theorem is_local_min.inf
added theorem is_local_min.max
added theorem is_local_min.min
added theorem is_local_min.neg
added theorem is_local_min.on
added theorem is_local_min.sub
added theorem is_local_min.sup
added def is_local_min
added theorem is_local_min_const
added theorem is_local_min_on.add
added theorem is_local_min_on.inf
added theorem is_local_min_on.inter
added theorem is_local_min_on.max
added theorem is_local_min_on.min
added theorem is_local_min_on.neg
added theorem is_local_min_on.sub
added theorem is_local_min_on.sup
added def is_local_min_on
added theorem is_local_min_on_const
added theorem is_max_on.is_local_max
added theorem is_max_on.localize
added theorem is_min_on.is_local_min
added theorem is_min_on.localize