Revision #1074 → #2465 · back to history
modifiedProduct limit definitionc4445c768190
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib defines Real.exp / NormedSpace.exp via a power series, not as the product limit (1 + x/n)^n; no declaration formalizes this alternative definition. |
| status | — | not_formalized |
modifiedPower series definitiona4786e492fc8
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | NormedSpace.exp_eq_tsum_div |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Normed.Algebra.Exponential |
| note | — | Mathlib's canonical definition of the exponential (NormedSpace.exp via NormedSpace.expSeries) is exactly this power series, and NormedSpace.exp_eq_tsum_div/NormedSpace.exp_eq_tsum witness the tsum form. |
| status | — | formalized |
modifiedInverse of logarithm integral definitionb04efe385120
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | Real.exp_log |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Basic |
| note | — | Real.log is defined via the exponential order-iso (not as ∫1/t) but Real.exp_log gives the inverse relationship and integral_one_div_of_pos ties the integral to log, so only the definitional route is missing. |
| status | — | partial |
modifiedDifferential equation definition226abe8ecd65
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | Real.hasDerivAt_exp |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.ExpDeriv |
| note | — | Mathlib proves Real.hasDerivAt_exp (exp'=exp) and Real.exp_zero=1, but does not define exp as the unique solution of y'=y with y(0)=1. |
| status | — | partial |
modifiedFunctional equation definitioncfa33d9399e0
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | Real.exp_add |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.Complex.Exponential |
| note | — | Real.exp_add / Complex.exp_add formalize the multiplicative property, but exp is not defined by this functional equation plus a regularity+normalization condition. |
| status | — | partial |
modifiedElementary definition by powers81e4cd89a413
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib's Real.rpow routes through exp/log rather than through a distinguished base b characterized by lim (b^h−1)/h = 1, so this elementary characterization is not present as a definition. |
| status | — | not_formalized |
modifiedError of product limit expressionfe414e0329c1
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib lemma bounds the difference exp(x) − (1+x/n)^n by the leading O(x^2/n) term of this expansion. |
| status | — | not_formalized |
modifiedConvergence of power seriesf6f4a29b9204
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | NormedSpace.expSeries_radius_eq_top |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Normed.Algebra.Exponential |
| note | — | NormedSpace.expSeries_radius_eq_top shows the exponential series has infinite radius of convergence, i.e. converges for every argument. |
| status | — | formalized |
modifiedLogarithm integral is a bijectiond23570e890ed
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | Real.expOrderIso |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Log.Basic |
| note | — | Real.expOrderIso (exp: ℝ ≃ ℝ>0) and Real.log_injOn_pos witness that log is a bijection ℝ>0 → ℝ, but not via the integral characterization. |
| status | — | partial |
modifiedExistence of base for elementary definition1be8e2b41ceb
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The claim that lim (b^h−1)/h exists for every b>0 and yields ln b is not stated in Mathlib as a standalone existence result driving an alternative definition. |
| status | — | not_formalized |
modifiedCharacterization 1 equivalent to Characterization 2922ce2cad937
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib theorem proves the product-limit form equals the power-series form of exp. |
| status | — | not_formalized |
modifiedCharacterization 1 equivalent to Characterization 3cf9903c8ea65
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib equivalence between the product-limit characterization and the inverse-of-∫1/t characterization is stated. |
| status | — | not_formalized |
modifiedCharacterization 1 equivalent to Characterization 434462eba89b5
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Euler-method argument connecting the product-limit definition to the ODE definition is not formalized. |
| status | — | not_formalized |
modifiedCharacterization 2 equivalent to Characterization 4ade61e640a81
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | hasDerivAt_exp |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Exponential |
| note | — | hasDerivAt_exp + NormedSpace.exp_zero establish that the power-series exp satisfies the ODE, but the reverse direction (uniqueness giving 4 ⇒ 2) is not packaged as an equivalence. |
| status | — | partial |
modifiedCharacterization 2 implies Characterization 5d9039f2a5992
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | Real.exp_add |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Exponential |
| note | — | Real.exp_add (and Complex.exp_add / NormedSpace.exp_add_of_commute) prove multiplicativity directly from the power-series definition. |
| status | — | formalized |
modifiedCharacterization 3 equivalent to Characterization 47d329fb4d53f
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib theorem states the equivalence of the inverse-of-∫1/t definition and the ODE definition of exp. |
| status | — | not_formalized |
modifiedCharacterization 5 implies Characterization 4779ed6faadb6
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib result derives the ODE characterization from the multiplicative-plus-regularity characterization. |
| status | — | not_formalized |
modifiedCharacterization 5 implies Characterization 4 (alternate)55cf619eb130
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The alternate proof deducing y'=y from f(x+y)=f(x)f(y) plus f'(0)=1 is not present in Mathlib. |
| status | — | not_formalized |
modifiedCharacterization 5 equivalent to Characterization 6685624a9c9c1
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not link the multiplicative-property characterization to the b^x elementary characterization as an if-and-only-if. |
| status | — | not_formalized |
modifiedLebesgue-integrability implies continuity (5 ⇒ 6)64ba9e10bcbe
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib lemma proves that a Lebesgue-integrable solution of the Cauchy multiplicative functional equation is continuous. |
| status | — | not_formalized |
modifiedCounterexample for complex initial conditions96b81fb5a6db
| Field | From #1074 | To #2465 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The counterexample showing that the characterizations fail on ℂ without further conditions is not formalized in Mathlib. |
| status | — | not_formalized |
addedNatural logarithm as integralb8da137d2613
addedExtension to complex domain via analytic continuation362b4dbb4bac
addedDefinitions (1), (2), (4) extend to Banach algebras65128cce2163
addedIntegrand 1/t is integrable, integral well-definedaabebaaace47
addedSurjectivity via divergence of harmonic series6d95d26cf4f0
addedIntermediate value theorem guarantees existence of base26b433eaf824
addedBinomial theorem bound in Rudin's argument09da0e939ef9
addedExtension of equivalence to negative reals278e52733191
addedFundamental theorem of calculus applied to ln11b505610e8d
addedLogarithm power rule ln(a^n) = n ln(a)b7af0a73e956
addedEuler's method converges to exact solution0d3a82591b0e
addedNonzero function is nonzero everywhere4ecb468fdb1c
addedContinuity at one point implies continuity everywhere2165953f6682