WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Elliptic integral

Revision #1183 → #2458 · back to history

modifiedElliptic integral (classical)d264cf77072b
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No elliptic-integral definition exists in Mathlib; a grep for `EllipticIntegral` returns nothing.
status—not_formalized
modifiedElliptic integral (modern)f0e2c84e8b21
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not define the general R(t, √P(t))-integral form.
status—not_formalized
modifiedReduction to Legendre canonical formsf820560de39e
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Legendre canonical forms and the reduction theorem are absent from Mathlib.
status—not_formalized
modifiedIncomplete elliptic integral of the first kind79b1ccb89994
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The function F(φ,k) is not defined in Mathlib.
status—not_formalized
modifiedJacobi's algebraic form of Fbd8d13807ea9
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the trigonometric nor the algebraic form of F is present in Mathlib.
status—not_formalized
modifiedF as inverse of snd47ae3ada462
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no Jacobi elliptic functions (sn/cn/dn) nor F.
status—not_formalized
modifiedAddition theorem for Ff334837a0f2f
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No addition formula for F is stated in Mathlib since F is not defined.
status—not_formalized
modifiedModulus transformation for F906daf829262
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modulus transformations for F are absent from Mathlib.
status—not_formalized
modifiedIncomplete elliptic integral of the second kind720d14ce3a3c
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The function E(φ,k) is not in Mathlib.
status—not_formalized
modifiedJacobi's algebraic form of Ea9a27b3f405c
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
addedRelations with Jacobi elliptic functions for E0ed04f197949
modifiedMeridian arc length via E88279c4de489
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Meridian-arc formula is not in Mathlib (no ellipsoid geodesy or E).
status—not_formalized
modifiedAddition theorem for Ec0d2170121c7
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Addition formula for E is absent.
status—not_formalized
modifiedModulus transformation for E277511f95f0a
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modulus transformation for E is not in Mathlib.
status—not_formalized
modifiedIncomplete elliptic integral of the third kindec2a3ea4410b
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Π(n; φ, k) is not defined in Mathlib.
status—not_formalized
modifiedCharacteristic n of Π3a16a38edb94
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized; Π is absent.
status—not_formalized
addedRelation of Π with Jacobi elliptic functionsef604994a591
modifiedMeridian arc length via Π07703bc9caec
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib (no Π, no geodesy).
status—not_formalized
modifiedComplete elliptic integral of the first kind13d6e7a4ff11
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—K(k) is not defined in Mathlib.
status—not_formalized
addedK via incomplete F at π/26ee079199035
modifiedPower series for K2e0da275dc72
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—K's binomial-squared series is not in Mathlib.
status—not_formalized
modifiedK via Gauss hypergeometric functionfe8f4c09addc
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no ₂F₁ Gauss hypergeometric (only `OrdinaryHypergeometric`) and no K.
status—not_formalized
modifiedK via arithmetic-geometric meanf42feffb5433
FieldFrom #1183To #2458
mathlib.decl—NNReal.agm
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
note—The AGM itself is formalized as `NNReal.agm`, but its identity with π/(2K) is not since K is undefined.
status—partial
modifiedModulus transformation for K3a06a74b10f1
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modulus transformations of K are absent.
status—not_formalized
modifiedK closed form via gamma function81017eefc138
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Chowla-Selberg / singular-moduli closed forms of K are not in Mathlib.
status—not_formalized
modifiedGamma closed form at r=2,3,702098f748017
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—These special K-values are not stated in Mathlib.
status—not_formalized
modifiedSufficient imaginary quadratic field condition7848bebd3416
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Chowla-Selberg criterion tying K(k) to Γ is not formalized.
status—not_formalized
modifiedAsymptotic expression for K5ed3f26681b6
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib (K itself is missing).
status—not_formalized
modifiedDifferential equation for K7fa2fe57d229
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Legendre ODE for K is not stated in Mathlib.
status—not_formalized
modifiedSecond solution of K differential equation16db845c822d
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedContinued fraction expansion of K9fcac77f3d69
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No continued-fraction expansion of K in Mathlib.
status—not_formalized
modifiedInverting the period ratio via modular lambda02a7b490fe15
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modular lambda function λ(τ) and this inversion are not in Mathlib.
status—not_formalized
modifiedError analysis for period ratio inversion314c2ecb0cd0
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedComplete elliptic integral of the second kind96cc6b074c73
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—E(k) is not defined in Mathlib.
status—not_formalized
addedComplete E via incomplete E at π/23de3774dadbf
modifiedEllipse circumference via Ebbf2a71baa14
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Ellipse arc-length formula via E is not in Mathlib.
status—not_formalized
modifiedPower series for complete Ebfa1c2eb447c
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedComplete E via Gauss hypergeometric functiona964a87640fa
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—₂F₁ representation of E is not in Mathlib.
status—not_formalized
modifiedModulus transformation for complete Ebf96c7d459e8
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modulus transformation of E is absent.
status—not_formalized
modifiedAGM computation of complete E62bb7c2a450c
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The AGM iteration is in `NNReal.agmSequences`, but the identity computing E is not stated because E is undefined.
status—not_formalized
modifiedQuadratic convergence of AGM for Ef8b885c24dd7
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—AGM's rate of convergence for E is not formalized (E is missing).
status—not_formalized
modifiedE closed form via gamma functiondd2c0d992acb
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Closed-form E via Γ is absent from Mathlib.
status—not_formalized
modifiedSecond solution for E differential equation0aa19dcf658d
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedComplete elliptic integral of the third kindd1e36a76b587
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Π(n, k) is not defined in Mathlib.
status—not_formalized
modifiedAlternative sign convention for Πa25496db108d
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No sign-convention variants of Π in Mathlib.
status—not_formalized
modifiedJacobi zeta function23d1d35ca5e3
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no Jacobi zeta function.
status—not_formalized
modifiedLegendre's relation (Pythagorean counterparts)1cccfda23774
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Legendre's relation E·K'+E'·K−K·K' = π/2 is not stated in Mathlib.
status—not_formalized
modifiedLegendre's relation (tangential counterparts)ceeb7d2d4225
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Tangential-modulus Legendre relation is not in Mathlib.
status—not_formalized
modifiedLemniscatic case of Legendre's identity15f72b6c4d39
FieldFrom #1183To #2458
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The lemniscatic special case (k = 1/√2) is not formalized.
status—not_formalized