Commit 2020-01-09 02:47 52899945

feat(analysis/calculus/mean_value): add generalized "fencing" inequality (#1838)

• feat(analysis/calculus/mean_value): add generalized "fencing" inequality This version can be used to deduce, e.g., Gronwall inequality as well as its generalized version that deals with approximate solutions.
• Adjust to merged branches, use liminf instead of limsup, add more variations
• Go through dim-1 liminf estimates
• Fix: use b ∈ Ioc a c as a hypothesis for I??_mem_nhds_within_Iio
• Update src/analysis/calculus/mean_value.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
• Drop Prop-valued variables, add some docs
• More docstrings
• Drop Prop-valued variables, drop assumption x ∉ s.