How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals). Let and let . Then is:
- nondecreasing when for all with ;
- increasing, or strictly increasing, when for all with ;
- nonincreasing when for all with ;
- decreasing, or strictly decreasing, when for all with ;
- monotone when it is nondecreasing or nonincreasing;
- strictly monotone when it is increasing or decreasing.
The naming follows the convention of Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences, which is the convention of this library throughout: increasing is the strict notion and nondecreasing the weak one.
An increasing function is nondecreasing, and a decreasing function is nonincreasing. For either , and then , hence ; or , and then . The same argument with the inequalities reversed gives the second claim. So strictly monotone implies monotone.
A strictly monotone function is injective (Injection, surjection, bijection). Let be increasing and let with . By trichotomy either , and then , or , and then ; in both cases . The decreasing case is the same argument. The converse fails, and the failure is not exotic: a continuous injection on an interval is strictly monotone (A continuous injective function on an interval is strictly monotone), but on a domain that is not an interval it need not be.
Negation exchanges the two directions. For , that is , the four conditions above are exchanged in pairs: is nondecreasing exactly when is nonincreasing, and is increasing exactly when is decreasing, because holds exactly when (Ordered field). Several proofs below use this to reduce a nonincreasing case to a nondecreasing one.
Monotone on a set, not at a point. All six conditions are conditions on the whole of ; unlike continuity (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point) there is no pointwise version, and none is used in this library. The domain is an arbitrary subset of ; where a result needs to be an interval (Intervals of : the nine order-convex forms, nondegeneracy, and length) it says so, and the hypothesis is never decoration.
The dictionary to monotone sequences
A sequence of reals is a function (Sequences of reals: bounded, eventually, frequently, tails, subsequences), and Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences calls it nondecreasing when for all , increasing when for all , and so on. Those are the same four conditions as above, read with the ordered set in place of the ordered subset and with the comparison of indices in place of the comparison of arguments. So nothing new is introduced here for sequences, and the two vocabularies may be used interchangeably: the words nondecreasing, increasing, nonincreasing, decreasing, monotone and strictly monotone mean the corresponding condition on the domain at hand.
One consequence is used repeatedly, and it has to be stated carefully because composition does not simply preserve the four words. Let be a nondecreasing sequence with for every , so that gives . Then:
- if is nondecreasing, is nondecreasing, since ;
- if is nonincreasing, is nonincreasing, since .
So along a nondecreasing sequence the composite inherits the direction of ; and with increasing and increasing, is increasing, while with increasing and decreasing, is decreasing.
Along a nonincreasing sequence the direction is reversed, not inherited. If is nonincreasing and is nonincreasing, then gives and hence : the composite is nondecreasing. The witness is on with , where both and are decreasing and is increasing. Two order-reversing maps compose to an order-preserving one, exactly as for the four words applied to functions.
Depends on
- Complete ordered field (least-upper-bound property)
- Order on the reals
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences
- Sequences of reals: bounded, eventually, frequently, tails, subsequences
- Ordered field
- Injection, surjection, bijection
Used by
- Abel's test for improper integrals Corollary
- An injective or monotone derivative on an interval is continuous Corollary
- The Cantor function is continuous on [0,1] Corollary
- A continuous injection on [0,1] ∪ [2,3] that is not monotone, so the interval hypothesis cannot be dropped from the strict-monotonicity theorem Counterexample
- Integrable φ and integrable f with φ∘ f not integrable: the order of the hypotheses in the composition theorem cannot be reversed Counterexample
- A singular function on a compact interval Definition
- Moduli of continuity and the Osgood divergence condition Definition
- Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral Definition
- The jump function of a nondecreasing function on a compact interval Definition
- ∫₀³ ⌊ x ⌋ = 3: the floor function is nondecreasing, hence integrable, and the integral is computed from the uniform partitions Example
- A bounded nondecreasing f : ℝ → ℝ whose set of discontinuities is exactly ℚ, obtained from the prescribed-jump construction applied to one fixed enumeration of the rationals Example
- A function with positive derivative at 0 that is monotone on no neighbourhood of 0 Example
- A step function integrated by additivity over subintervals, and the same value from the definition Example
- An additive f : ℝ → ℝ that is not x ↦ cx: the coefficient of one fixed Hamel basis vector. It is unbounded above and below on every nondegenerate interval, its graph is dense in ℝ², and every nonempty level set is dense in ℝ Example
- Froda's countable bound is attained: a bounded nondecreasing function on ℝ discontinuous exactly at the points 1 - 1/(k+1) for k ∈ ℕ, an infinite discontinuity set inside a bounded interval Example
- H(x) = 2√x on [0,1]: H is continuous, H' is unbounded on (0,1], and H' is therefore not Riemann integrable Example
- The integral test applied to ∑ 1/ι(k+1)ᵖ for rational p>0, cross-checked against the published p-series theorem Example
- The n-th root as a continuous inverse: for a natural n ≥ 1 the map x ↦ xⁿ is continuous and strictly increasing on [0,∞) with image [0,∞), so its inverse x ↦ x^1/n is continuous and strictly increasing Example
- x ↦ x³ is increasing on ℝ although its derivative vanishes at 0, which is the witness for the false statement that a vanishing derivative forbids strict increase, and which makes its inverse non-differentiable at 0 Example
- FALSE: every function of bounded variation is absolutely continuous False statement
- FALSE: if f'(c) = 0 then f is not increasing on any interval containing c False statement
- An injective Darboux function on an interval is strictly monotone Lemma
- The positive and negative variations are nondecreasing and give the Jordan identities Lemma
- The Cantor function is continuous and nondecreasing, climbs from 0 to 1, and is constant on every interval removed in the construction of the Cantor set, so all of its increase happens on a set of measure zero Remark
- A continuous function of a Stieltjes-integrable function is Stieltjes integrable for a nondecreasing integrator Theorem
- A continuous injective function on an interval is strictly monotone Theorem
- A convex function on an open interval is differentiable except at at most countably many points Theorem
- A differentiable function on an open interval is convex if and only if its derivative is nondecreasing Theorem
- A monotone function is differentiable almost everywhere by the Lebesgue-Stieltjes route Theorem
- A monotone function on [a,b] is Riemann integrable: for the uniform partition into N parts the upper minus lower sum telescopes to |f(b) - f(a)| (b-a)/ι(N) Theorem
- A monotone function on an interval has no discontinuity of the second kind: at every point both relevant one-sided limits exist, and an interior point c is a discontinuity exactly when lim_x → c⁻ f(x) < lim_x → c⁺ f(x) Theorem
- A nondecreasing function splits uniquely into a jump part and a continuous part Theorem
- Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal Theorem
- Bonnet's second mean value theorem: for f monotone and g integrable on [a,b] there is ξ∈[a,b] with ∫ₐᵇ fg = f(a)∫ₐ^ξ g + f(b)∫_ξᵇ g Theorem
- Change of variable in an improper integral Theorem
- Continuous inverse theorem: a continuous injective f on an interval I is a bijection onto the order-convex set f[I], and the inverse g : f[I] → I is continuous and strictly monotone in the same sense as f Theorem
- Converse to Froda: for every at most countable E ⊆ ℝ there is a bounded nondecreasing f : ℝ → ℝ whose set of discontinuities is exactly E, every one of them a jump Theorem
- Dirichlet's test for improper integrals Theorem
- Every monotone real function is Borel measurable Theorem
- For a nondecreasing function, the derivative is measurable and integrable and its integral is bounded by the total increase Theorem
…and 9 more results.
Dependency tree · two levels
20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Monotonic function (Wikipedia) (standard reference, not scraped)
- Monotone Functions (Analysis WebNotes) (standard reference, not scraped)