Revision #1209 → #1823 · back to history
modifiedBasic exponential formula with time constant53191ddf8245
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Basic formula","snippet":"A quantity x depends exponentially on time t"},{"type":"math_alttext","value":"{\\displaystyle x(t)=a\\cdot b^{t/\\tau }}"},{"type":"math_alttext","value":"{\\displaystyle x(0)=a\\,,}"},{"type":"math_alttext","value":"{\\displaystyle x(t+\\tau )=a\\cdot b^{(t+\\tau )/\\tau }=a\\cdot b^{t/\\tau }\\cdot b^{\\tau /\\tau }=x(t)\\cdot b\\,.}"}] | — |
modifiedEquivalent forms via change of base0fb07a96438e
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Basic formula","snippet":"Thus the law of exponential growth can be written in different but mathematically equivalent forms, by using a different base"},{"type":"math_alttext","value":"{\\displaystyle x(t)=x_{0}\\cdot e^{kt}=x_{0}\\cdot e^{t/\\tau }=x_{0}\\cdot 2^{t/T}=x_{0}\\cdot \\left(1+{\\frac {r}{100}}\\right)^{t/p},}"}] | — |
modifiedOne-to-one connection between k, τ, T, r065ac1fadf19
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Basic formula","snippet":"have a one-to-one connection given by the following equation"},{"type":"math_alttext","value":"{\\displaystyle k={\\frac {1}{\\tau }}={\\frac {\\ln 2}{T}}={\\frac {\\ln \\left(1+{\\frac {r}{100}}\\right)}{p}}}"}] | — |
modifiedLog-linear reformulation74b98392da12
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Reformulation as log-linear growth","snippet":"then the log (to any base) of x grows linearly over time, as can be seen by taking logarithms of both sides of the exponential growth equation"},{"type":"math_alttext","value":"{\\displaystyle \\log x(t)=\\log x_{0}+t\\cdot \\log(1+r).}"}] | — |
modifiedExponential function satisfies linear ODE32439a964a65
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Differential equation","snippet":"satisfies the linear differential equation"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {dx}{dt}}=kx}"}] | — |
| mathlib.match_kind | exact | special_case |
| note | `Real.hasDerivAt_exp : HasDerivAt exp (exp x) x` (and `Real.deriv_exp : deriv exp = exp`) state that `exp` solves `x' = x`. | `Real.hasDerivAt_exp : HasDerivAt exp (exp x) x` solves the k=1 case `x' = x`; the general `x' = kx` characterization with arbitrary `k` is not packaged as a single named theorem. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedSolution by direct integration92f96117139c
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Differential equation","snippet":"The differential equation is solved by direct integration"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{\\frac {dx}{dt}}&=kx\\\\[5pt]{\\frac {dx}{x}}&=k\\,dt\\\\[5pt]\\int _{x_{0}}^{x(t)}{\\frac {dx}{x}}&=k\\int _{0}^{t}\\,dt\\\\[5pt]\\ln {\\frac {x(t)}{x_{0}}}&=kt.\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle x(t)=x_{0}e^{kt}.}"}] | — |
| mathlib.module | Mathlib.Analysis.ODE.Gronwall | Mathlib.Analysis.ODE.ExistUnique |
modifiedExponential dominates polynomial growthcd785fabeb91
| Field | From #1209 | To #1823 |
|---|
| anchors | [{"section":"Other growth rates","snippet":"exponential growth of any kind will overtake linear growth of any kind"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{t\\to \\infty }{\\frac {t^{\\alpha }}{ae^{t}}}=0.}"}] | — |
| mathlib.decl | Real.isLittleO_rpow_exp_atTop | isLittleO_rpow_exp_atTop |
| note | `Real.isLittleO_rpow_exp_atTop` shows `x ^ s =o[atTop] exp` for any real `s`, formalizing that exponentials dominate polynomial growth. | `isLittleO_rpow_exp_atTop` shows `x ^ s =o[atTop] Real.exp` for any real `s`, formalizing that exponentials dominate polynomial growth. |
addedLogistic growthd13146451cd0
addedCompound interestab47be887f43
addedExponential complexity 2^x doubles per unit input5225d9254714