Revision #1309 → #2032 · back to history
modifiedHyperbolic functions (geometric)f09123b427b7
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.sinh |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | Mathlib defines the hyperbolic family (`Real.sinh`/`cosh`/`tanh` and `Complex` versions) although not via the geometric framing. |
| status | — | formalized |
modifiedDerivatives of sinh and coshec446089ad37
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.deriv_sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | `Real.deriv_sinh : deriv sinh = cosh` and `Real.deriv_cosh : deriv cosh = sinh` are both in DerivHyp. |
| status | — | formalized |
modifiedHyperbolic sine5668b47e6fc3
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Real.sinh` (and `Complex.sinh`) are defined in `Mathlib.Analysis.Complex.Trigonometric`. |
| status | — | formalized |
modifiedHyperbolic cosine7ee178637c3b
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.cosh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Real.cosh` and `Complex.cosh` are defined as `(exp z + exp (-z))/2`. |
| status | — | formalized |
modifiedHyperbolic tangentafc315161386
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.tanh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Real.tanh` and `Complex.tanh` are defined as `sinh/cosh`. |
| status | — | formalized |
modifiedHyperbolic cotangent930aebec22cf
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `coth`/`Real.coth`/`Complex.coth` declaration is present in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic secant5541631431f7
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `sech` declaration is present in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic cosecant7079baef41fa
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `csch` declaration is present in Mathlib. |
| status | — | not_formalized |
modifiedInverse hyperbolic functions2b7f704a5be6
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.arsinh |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Arsinh |
| note | — | `Real.arsinh`, `Real.arcosh`, `Real.artanh` are defined; the other three inverses (arcoth/arsech/arcsch) are absent. |
| status | — | partial |
modifiedHyperbolic anglee2d8138254a6
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of hyperbolic angle / hyperbolic sector area in Mathlib. |
| status | — | not_formalized |
modifiedsinh and cosh are entire4b1239d14fa9
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.analyticOnNhd_sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | `Complex.analyticOnNhd_sinh`/`analyticOnNhd_cosh` (and `differentiable_sinh`/`differentiable_cosh`) state that they are entire. |
| status | — | formalized |
modifiedOther hyperbolic functions meromorphic74f72019cf48
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.meromorphic_tanh |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic |
| note | — | Only `Complex.meromorphic_tanh` is formalized; coth/sech/csch are not even defined. |
| status | — | partial |
modifiedTranscendence via Lindemann–Weierstrass0b349a2e8f30
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | LindemannWeierstrass.exp_polynomial_approx |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart |
| note | — | Only the analytical part of Lindemann–Weierstrass is in Mathlib; the corollary for hyperbolic values is not stated. |
| status | — | partial |
modifiedExponential definition (sinh and cosh)c88729ff97bf
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.sinh_eq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Real.sinh_eq`/`Real.cosh_eq` give the exponential formulas; the Complex versions are the literal definitions. |
| status | — | formalized |
modifiedHyperbolic sine as odd part of exp4ccf7eaf821f
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | The Mathlib definition `Complex.sinh z = (exp z - exp (-z))/2` is literally the odd part of `exp`. |
| status | — | formalized |
modifiedHyperbolic cosine as even part of expeffdad0d581d
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.cosh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.cosh z := (exp z + exp (-z))/2` is the even part of `exp`. |
| status | — | formalized |
modifiedHyperbolic tangent (exponential)17d8ab9332c4
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.tanh_eq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Real.tanh_eq` gives `tanh x = (exp x - exp(-x))/(exp x + exp(-x))`. |
| status | — | formalized |
modifiedHyperbolic cotangent (exponential)28833fde6f96
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No coth function or exponential identity for it is in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic secant (exponential)3896bb40d26b
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No sech function is defined in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic cosecant (exponential)9d614b243536
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No csch function is defined in Mathlib. |
| status | — | not_formalized |
modifiedSinh and cosh via ODE systeme38d5d8ae928
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.hasDerivAt_sinh |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | Mathlib has `hasDerivAt_sinh`/`hasDerivAt_cosh` (so sinh'=cosh, cosh'=sinh) but does not characterize sinh/cosh as the unique solution of this ODE system. |
| status | — | partial |
modifiedSinh and cosh as solutions of f''=fa6df5b406dfe
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.deriv_sinh |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | That sinh''=sinh and cosh''=cosh is derivable from `deriv_sinh = cosh`/`deriv_cosh = sinh`, but the uniqueness statement is not formalized. |
| status | — | partial |
modifiedHyperbolic functions via complex trig5b088a820c4f
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh_mul_I |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.sinh_mul_I : sinh (x*I) = sin x * I` and `Complex.cosh_mul_I : cosh (x*I) = cos x` capture this relationship. |
| status | — | formalized |
modifiedArea under cosh equals arc length79f4a8c72685
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No statement about area-under-cosh equalling arc length is in Mathlib. |
| status | — | not_formalized |
modifiedTanh as ODE solutionc635c7164dbf
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No ODE-uniqueness characterization of tanh is in Mathlib. |
| status | — | not_formalized |
modifiedOsborn's rule38d84029d5e6
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Osborn's rule (sign convention for converting trig identities to hyperbolic) is not formalized. |
| status | — | not_formalized |
modifiedOdd and even functions8bf9e3d63d26
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh_neg |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `sinh_neg : sinh (-x) = -sinh x` and `cosh_neg : cosh (-x) = cosh x` are in Mathlib for both `Real` and `Complex`. |
| status | — | formalized |
modifiedReciprocals581e5a05df10
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Since coth/sech/csch are not defined, their reciprocal identities are not formalized. |
| status | — | not_formalized |
modifiedAnalogue of Euler's formula98117c0ab933
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.cosh_add_sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.cosh_add_sinh : cosh x + sinh x = exp x` (and `Real` version) formalize the hyperbolic Euler analogue. |
| status | — | formalized |
modifiedHyperbolic Pythagorean identityb6eb7993ed32
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.cosh_sq_sub_sinh_sq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1` (and Real version). |
| status | — | formalized |
modifiedSums and differences of argumentsdf5b275c3ef7
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh_add |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.sinh_add`, `cosh_add`, `sinh_sub`, `cosh_sub` are all in Mathlib for `Real` and `Complex`. |
| status | — | formalized |
modifiedHalf argument formulas29201ac6b365
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Half-angle formulas for sinh/cosh in terms of the sign function are not formalized for arbitrary real arguments. |
| status | — | not_formalized |
modifiedHalf argument formula for nonzero x68a8cc9660e5
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The half-argument formula for nonzero x is not in Mathlib. |
| status | — | not_formalized |
modifiedTangent half argument formulaa3e85fbdf5c5
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No tanh half-argument formula appears in Mathlib. |
| status | — | not_formalized |
modifiedStatistical inequality for hyperbolic functionsdb97b1293a6f
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.cosh_le_exp_half_sq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Series |
| note | — | `Real.cosh_le_exp_half_sq : cosh x ≤ exp (x^2/2)` is the inequality used in statistics (e.g. Hoeffding). |
| status | — | formalized |
modifiedSinh and cosh equal their second derivativesf9485269c656
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.deriv_sinh |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | Follows directly from `deriv_sinh = cosh` and `deriv_cosh = sinh`, but no dedicated `sinh'' = sinh` lemma is stated. |
| status | — | partial |
modifiedFunctions equal to own second derivativee2683eeb065c
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No general classification of solutions of f''=f as span{sinh,cosh} is formalized. |
| status | — | not_formalized |
modifiedIntegrals via hyperbolic substitutiona8e0d260096c
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Integrals of 1/√(x²±a²), etc. via hyperbolic substitution are not in Mathlib. |
| status | — | not_formalized |
modifiedTaylor series of sinhd36f109a5b99
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.sinh_eq_tsum |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Series |
| note | — | `Real.sinh_eq_tsum`/`Complex.sinh_eq_tsum` give `sinh x = ∑ x^(2n+1)/(2n+1)!`. |
| status | — | formalized |
modifiedTaylor series of cosh4d61733380ce
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Real.cosh_eq_tsum |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Series |
| note | — | `Real.cosh_eq_tsum`/`Complex.cosh_eq_tsum` give `cosh x = ∑ x^(2n)/(2n)!`. |
| status | — | formalized |
modifiedSum of sinh and cosh seriesa2be5ea5045b
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh_add_cosh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.sinh_add_cosh : sinh x + cosh x = exp x` (plus the tsum identities) gives this; combined with `cosh_eq_tsum`/`sinh_eq_tsum` the series-sum form follows. |
| status | — | formalized |
modifiedInfinite product expansionsea3e907aff69
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Weierstrass-product expansions of sinh/cosh appear in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic angle invariance under squeeze mapping509649c72f6b
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of squeeze mappings or hyperbolic-angle invariance. |
| status | — | not_formalized |
modifiedGudermannian function relation81e80700abd6
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The Gudermannian function is not defined in Mathlib. |
| status | — | not_formalized |
modifiedCatenary as graph of cosh6373f5ca475c
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The catenary curve is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedExponential decomposition into sinh and coshb7fea8e8bd4c
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.cosh_add_sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.cosh_add_sinh : cosh x + sinh x = exp x` and `Complex.cosh_sub_sinh : cosh x - sinh x = exp (-x)` give the decomposition. |
| status | — | formalized |
modifiedHyperbolic functions for complex arguments8a4fdc94dcdd
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Complex.Trigonometric |
| note | — | `Complex.sinh`, `Complex.cosh`, `Complex.tanh` are defined directly on `ℂ`. |
| status | — | formalized |
modifiedsinh z and cosh z are holomorphic1d2c2bb13095
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.analyticOnNhd_sinh |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp |
| note | — | `Complex.analyticOnNhd_sinh`/`analyticOnNhd_cosh` (and `differentiable_sinh`/`differentiable_cosh`) state holomorphicity. |
| status | — | formalized |
modifiedPeriodicity in imaginary component59e0628334ed
| Field | From #1309 | To #2032 |
|---|
| mathlib.decl | — | Complex.sinh_periodic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |
| note | — | `Complex.sinh_periodic`/`cosh_periodic` give period `2π·I`, and `tanh_periodic` gives period `π·I`. |
| status | — | formalized |
addedAddition and subtraction formulas123458161628
addedProduct formulas92f9ce61f1f9
addedSquare formulas2567832d168d
addedInverse hyperbolic functions as logarithms879452098363
addedDerivatives of hyperbolic functions261b94e44c2d
addedStandard integrals of hyperbolic functions239f4949e719
addedTaylor series convergence on complex plane (sinh)9a34fda8f8dd
addedTaylor series convergence on complex plane (cosh)5d9edb3a5df2
addedCircular sector area equals angle when r=√2b5c9c560da68
addedComplex exponential via sinh and cosh5d3bde79aabe