Special Functions

Results named in Tau Ceti's TauCeti.Analysis.SpecialFunctions modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe addition theorem for cn (DLMF 22.8.2)#

cn(u + v) = (cn u · cn v - sn u · dn u · sn v · dn v) / (1 - k² sn²(u) sn²(v)).

TauCeti.Real.jacobiCn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) :
  TauCeti.Real.jacobiCn k (u + v) =
    (TauCeti.Real.jacobiCn k u * TauCeti.Real.jacobiCn k v -
        TauCeti.Real.jacobiSn k u * TauCeti.Real.jacobiDn k u * TauCeti.Real.jacobiSn k v *
          TauCeti.Real.jacobiDn k v) /
      (1 - k ^ 2 * TauCeti.Real.jacobiSn k u ^ 2 * TauCeti.Real.jacobiSn k v ^ 2)
Lean

Formalized in Tau Ceti as TauCeti.Real.jacobiCn_add.

Sources
LeanTauCeti.Real.jacobiCn_add

TheoremThe addition theorem for dn (DLMF 22.8.3)#

dn(u + v) = (dn u · dn v - k² · sn u · cn u · sn v · cn v) / (1 - k² sn²(u) sn²(v)).

TauCeti.Real.jacobiDn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) :
  TauCeti.Real.jacobiDn k (u + v) =
    (TauCeti.Real.jacobiDn k u * TauCeti.Real.jacobiDn k v -
        k ^ 2 * TauCeti.Real.jacobiSn k u * TauCeti.Real.jacobiCn k u * TauCeti.Real.jacobiSn k v *
          TauCeti.Real.jacobiCn k v) /
      (1 - k ^ 2 * TauCeti.Real.jacobiSn k u ^ 2 * TauCeti.Real.jacobiSn k v ^ 2)
Lean

Formalized in Tau Ceti as TauCeti.Real.jacobiDn_add.

Sources
LeanTauCeti.Real.jacobiDn_add

TheoremThe addition theorem for sn (DLMF 22.8.1)#

sn(u + v) = (sn u · cn v · dn v + sn v · cn u · dn u) / (1 - k² sn²(u) sn²(v)).

TauCeti.Real.jacobiSn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) :
  TauCeti.Real.jacobiSn k (u + v) =
    (TauCeti.Real.jacobiSn k u * TauCeti.Real.jacobiCn k v * TauCeti.Real.jacobiDn k v +
        TauCeti.Real.jacobiSn k v * TauCeti.Real.jacobiCn k u * TauCeti.Real.jacobiDn k u) /
      (1 - k ^ 2 * TauCeti.Real.jacobiSn k u ^ 2 * TauCeti.Real.jacobiSn k v ^ 2)
Lean

Formalized in Tau Ceti as TauCeti.Real.jacobiSn_add.

Sources
LeanTauCeti.Real.jacobiSn_add

TheoremThe addition theorem for ℘'#

If z, w ∉ Λ and ℘(z) ≠ ℘(w), then ℘'(z + w) = -m (℘(z + w) - ℘(z)) - ℘'(z) with m = (℘'(z) - ℘'(w)) / (℘(z) - ℘(w)): the points (℘(z), ℘'(z)), (℘(w), ℘'(w)) and (℘(z + w), -℘'(z + w)) lie on a line of slope m.

PeriodPair.derivWeierstrassP_add (L : PeriodPair) {z w : ℂ} (hz : z ∉ L.lattice)
  (hw : w ∉ L.lattice) (h : L.weierstrassP z ≠ L.weierstrassP w) :
  L.derivWeierstrassP (z + w) =
    -((L.derivWeierstrassP z - L.derivWeierstrassP w) / (L.weierstrassP z - L.weierstrassP w)) *
        (L.weierstrassP (z + w) - L.weierstrassP z) -
      L.derivWeierstrassP z
Lean

Formalized in Tau Ceti as PeriodPair.derivWeierstrassP_add.

Sources
LeanPeriodPair.derivWeierstrassP_add
Uses 1
Proof usesThe addition theorem for ℘

TheoremThe addition theorem for ℘#

If z, w ∉ Λ and ℘(z) ≠ ℘(w), then ℘(z + w) = ((℘'(z) - ℘'(w)) / (℘(z) - ℘(w)))² / 4 - ℘(z) - ℘(w).

PeriodPair.weierstrassP_add (L : PeriodPair) {z w : ℂ} (hz : z ∉ L.lattice) (hw : w ∉ L.lattice)
  (h : L.weierstrassP z ≠ L.weierstrassP w) :
  L.weierstrassP (z + w) =
    ((L.derivWeierstrassP z - L.derivWeierstrassP w) / (L.weierstrassP z - L.weierstrassP w)) ^ 2 /
          4 -
        L.weierstrassP z -
      L.weierstrassP w
Lean

Formalized in Tau Ceti as PeriodPair.weierstrassP_add.

Sources
LeanPeriodPair.weierstrassP_add
Used by 1
Used byThe addition theorem for ℘'

TheoremBernstein's exponential bound#

If x ≤ c with 0 ≤ c < 3, then exp x ≤ 1 + x + x ^ 2 / (2 * (1 - c / 3)). Only an upper bound on x is needed: negative x are covered by Real.exp_le_one_add_add_sq_div_two_of_nonpos.

Real.exp_le_one_add_add_sq_div_of_le {x c : ℝ} (hxc : x ≤ c) (hc0 : 0 ≤ c) (hc3 : c < 3) :
  Real.exp x ≤ 1 + x + x ^ 2 / (2 * (1 - c / 3))
Lean

Formalized in Tau Ceti as Real.exp_le_one_add_add_sq_div_of_le.

Sources
LeanReal.exp_le_one_add_add_sq_div_of_le
Used by 1
Used byBernstein's moment-generating-function bound

TheoremThe duplication theorem for R_F (DLMF 19.26.18) at nonnegative real arguments#

for real x, y, z ≥ 0, with λ = √x √y + √y √z + √z √x, R_F(x, y, z) = R_F((x + λ)/4, (y + λ)/4, (z + λ)/4).

No hypothesis beyond nonnegativity is needed. When two of x, y, z vanish, the defining integrals on both sides diverge and the identity is between the totalized values 0.

Complex.carlsonRF_ofReal_duplication {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) :
  have l := √x * √y + √y * √z + √z * √x;
  (↑x).carlsonRF ↑y ↑z = (↑((x + l) / 4)).carlsonRF ↑((y + l) / 4) ↑((z + l) / 4)
Lean

Formalized in Tau Ceti as Complex.carlsonRF_ofReal_duplication.

Sources
LeanComplex.carlsonRF_ofReal_duplication

TheoremEuler's limit formula in ratio form#

For every real s, Γ(n + 1 + s) is asymptotic to n ^ s * n! as the natural number n tends to infinity.

Real.isEquivalent_Gamma_natCast_add_one_add (s : ℝ) :
  Asymptotics.IsEquivalent Filter.atTop (fun n => Real.Gamma (↑n + 1 + s)) fun n =>
    ↑n ^ s * ↑n.factorial
Lean

Formalized in Tau Ceti as Real.isEquivalent_Gamma_natCast_add_one_add.

Sources
LeanReal.isEquivalent_Gamma_natCast_add_one_add

TheoremFatou's lemma on circles#

If log⁺ ‖f‖⁻¹ is integrable on the circles about c of radii ρ n, and its circle averages there are at most B, then the angles in one period along which f (circleMap c (ρ n) θ) tends to 0 through nonzero values form a null set.

TauCeti.volume_setOf_tendsto_circleMap_nhdsNE_zero {f : ℂ → ℂ} {c : ℂ} {ρ : ℕ → ℝ} {B : ℝ}
  (hf : ∀ (n : ℕ), CircleIntegrable (fun z => ‖f z‖⁻¹.posLog) c (ρ n))
  (hB : ∀ (n : ℕ), Real.circleAverage (fun z => ‖f z‖⁻¹.posLog) c (ρ n) ≤ B) :
  MeasureTheory.volume
      {θ |
        θ ∈ Set.Ioc 0 (2 * Real.pi) ∧
          Filter.Tendsto (fun n => f (circleMap c (ρ n) θ)) Filter.atTop (nhdsWithin 0 {0}ᶜ)} =
    0
Lean

Formalized in Tau Ceti as TauCeti.volume_setOf_tendsto_circleMap_nhdsNE_zero.

Sources
LeanTauCeti.volume_setOf_tendsto_circleMap_nhdsNE_zero
Used by 1
Used byCoburn's alternative

TheoremGauss's identity#

the lemniscate constant is ϖ = π / M(1, √2), where M is the arithmetic-geometric mean NNReal.agm.

TauCeti.Real.lemniscateConstant_eq_pi_div_agm :
  TauCeti.Real.lemniscateConstant = Real.pi / ↑(NNReal.agm 1 (NNReal.sqrt 2))
Lean

Formalized in Tau Ceti as TauCeti.Real.lemniscateConstant_eq_pi_div_agm.

Sources
LeanTauCeti.Real.lemniscateConstant_eq_pi_div_agm
Uses 1
Proof usesGauss's theorem

TheoremGauss's theorem#

for k ^ 2 < 1, the complete elliptic integral of the first kind is K(k) = π / (2 M(1, k')), where M is the arithmetic-geometric mean and k' = √(1 - k²) is the complementary modulus.

TauCeti.Real.legendreK_eq_pi_div_two_mul_agm {k : ℝ} (hk : k ^ 2 < 1) :
  TauCeti.Real.legendreK k = Real.pi / (2 * ↑(NNReal.agm 1 (√(1 - k ^ 2)).toNNReal))
Lean

Formalized in Tau Ceti as TauCeti.Real.legendreK_eq_pi_div_two_mul_agm.

Sources
LeanTauCeti.Real.legendreK_eq_pi_div_two_mul_agm
Used by 2
Used byGauss's identity · Salamin's formula for complementary moduli

TheoremThe Gauss–Brent–Salamin formula#

with the AGM iteration a₀ = 1, g₀ = 1 / √2 and cⱼ² = aⱼ² - gⱼ², π = 4 M(1, 1/√2)² / (1 - ∑_{j ≥ 1} 2^(j+1) cⱼ²). Mathlib's agmSequences 1 (√2)⁻¹ n is the pair (gₙ₊₁, aₙ₊₁), so the series index is n = j - 1.

TauCeti.Real.pi_eq_four_mul_agm_sq_div_one_sub_tsum :
  Real.pi =
    4 * ↑(NNReal.agm 1 (NNReal.sqrt 2)⁻¹) ^ 2 /
      (1 -
        ∑' (n : ℕ),
          2 ^ (n + 2) *
            (↑(NNReal.agmSequences 1 (NNReal.sqrt 2)⁻¹ n).2 ^ 2 -
              ↑(NNReal.agmSequences 1 (NNReal.sqrt 2)⁻¹ n).1 ^ 2))
Lean

Formalized in Tau Ceti as TauCeti.Real.pi_eq_four_mul_agm_sq_div_one_sub_tsum.

Sources
LeanTauCeti.Real.pi_eq_four_mul_agm_sq_div_one_sub_tsum
Uses 1
Proof usesSalamin's formula for complementary moduli

TheoremJordan's integral bound#

For c > 0, ∫₀^π e^{-c sin θ} dθ < π / c.

TauCeti.integral_exp_neg_mul_sin_lt (c : ℝ) (hc : 0 < c) :
  ∫ (θ : ℝ) in 0..Real.pi, Real.exp (-c * Real.sin θ) < Real.pi / c
Lean

Formalized in Tau Ceti as TauCeti.integral_exp_neg_mul_sin_lt.

Sources
LeanTauCeti.integral_exp_neg_mul_sin_lt
Used by 1
Used byJordan's lemma

TheoremPeetre's inequality (TauCeti.one_add_norm_add_sq_rpow_le_mul)#

For every real s, the Japanese bracket ⟨x⟩ = (1 + ‖x‖ ^ 2) ^ (1/2) satisfies ⟨x + y⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x⟩ ^ s ⟨y⟩ ^ |s|.

TauCeti.one_add_norm_add_sq_rpow_le_mul.{u_1} {E : Type u_1} [SeminormedAddGroup E] (s : ℝ)
  (x y : E) :
  (1 + ‖x + y‖ ^ 2) ^ (s / 2) ≤ 2 ^ (|s| / 2) * (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖y‖ ^ 2) ^ (|s| / 2)
Lean

Formalized in Tau Ceti as TauCeti.one_add_norm_add_sq_rpow_le_mul.

Other forms

Peetre's inequality. Formalized in Tau Ceti as TauCeti.one_add_norm_sq_rpow_le_mul_sub.

TauCeti.one_add_norm_sq_rpow_le_mul_sub.{u_1} {E : Type u_1} [SeminormedAddCommGroup E] (s : ℝ)
  (x y : E) :
  (1 + ‖x‖ ^ 2) ^ (s / 2) ≤ 2 ^ (|s| / 2) * (1 + ‖x - y‖ ^ 2) ^ (|s| / 2) * (1 + ‖y‖ ^ 2) ^ (s / 2)

Peetre's inequality, subadditive form. Formalized in Tau Ceti as TauCeti.one_add_norm_add_sq_rpow_le.

TauCeti.one_add_norm_add_sq_rpow_le.{u_1} {E : Type u_1} [SeminormedAddGroup E] {s : ℝ} (hs : 0 ≤ s)
  (x y : E) :
  (1 + ‖x + y‖ ^ 2) ^ (s / 2) ≤ 2 ^ s * ((1 + ‖x‖ ^ 2) ^ (s / 2) + (1 + ‖y‖ ^ 2) ^ (s / 2))
Sources
LeanTauCeti.one_add_norm_add_sq_rpow_le_mul · TauCeti.one_add_norm_sq_rpow_le_mul_sub · TauCeti.one_add_norm_add_sq_rpow_le

TheoremSalamin's formula for complementary moduli#

if x, y > 0 and x² + y² = 1, then π = 4 M(1, x) M(1, y) / (1 - ∑ₙ 2ⁿ⁺¹ (cₙ₊₁(x)² + cₙ₊₁(y)²)), where M is the AGM and cₙ₊₁(x)² = aₙ₊₁² - gₙ₊₁² is the squared correction of the AGM iteration started at (1, x). Mathlib's agmSequences 1 x n is the pair (gₙ₊₁, aₙ₊₁).

TauCeti.Real.pi_eq_four_mul_agm_mul_agm_div_one_sub_tsum {x y : NNReal} (hx : 0 < x) (hy : 0 < y)
  (hxy : x ^ 2 + y ^ 2 = 1) :
  Real.pi =
    4 * ↑(NNReal.agm 1 x) * ↑(NNReal.agm 1 y) /
      (1 -
        ∑' (n : ℕ),
          2 ^ (n + 1) *
            (↑(NNReal.agmSequences 1 x n).2 ^ 2 - ↑(NNReal.agmSequences 1 x n).1 ^ 2 +
              (↑(NNReal.agmSequences 1 y n).2 ^ 2 - ↑(NNReal.agmSequences 1 y n).1 ^ 2)))
Lean

Formalized in Tau Ceti as TauCeti.Real.pi_eq_four_mul_agm_mul_agm_div_one_sub_tsum.

Sources
LeanTauCeti.Real.pi_eq_four_mul_agm_mul_agm_div_one_sub_tsum
Uses 1 · Used by 1
Proof usesGauss's theorem
Used byThe Gauss–Brent–Salamin formula

TheoremThe scalar Bellman majorization estimate#

For 2 ≤ p and x, y ≥ 0, ((p - 1) ^ (p - 1) / p ^ (p - 2)) Φ_p(x, y) ≤ (p - 1) ^ p x ^ p - y ^ p.

TauCeti.mul_burkholderPhi_le {p : ℝ} (hp : 2 ≤ p) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
  (p - 1) ^ (p - 1) / p ^ (p - 2) * TauCeti.burkholderPhi p x y ≤ (p - 1) ^ p * x ^ p - y ^ p
Lean

Formalized in Tau Ceti as TauCeti.mul_burkholderPhi_le.

Sources
LeanTauCeti.mul_burkholderPhi_le

TheoremThe scalar Bellman midpoint estimate#

For 2 ≤ p, real x, y, a and ε with |ε| = 1, 2 Φ_p(|x|, |y|) ≤ Φ_p(|x + a|, |y + ε a|) + Φ_p(|x - a|, |y - ε a|).

TauCeti.two_mul_burkholderPhi_abs_le {p : ℝ} (hp : 2 ≤ p) (x y a : ℝ) {ε : ℝ} (hε : |ε| = 1) :
  2 * TauCeti.burkholderPhi p |x| |y| ≤
    TauCeti.burkholderPhi p |x + a| |y + ε * a| + TauCeti.burkholderPhi p |x - a| |y - ε * a|
Lean

Formalized in Tau Ceti as TauCeti.two_mul_burkholderPhi_abs_le.

Sources
LeanTauCeti.two_mul_burkholderPhi_abs_le

TheoremThe uniformization theorem#

for all a, b ∈ ℂ with a³ - 27 b² ≠ 0 there is a lattice Λ with g₂(Λ) = a and g₃(Λ) = b.

PeriodPair.exists_g₂_g₃_eq {a b : ℂ} (hab : a ^ 3 - 27 * b ^ 2 ≠ 0) : ∃ L, L.g₂ = a ∧ L.g₃ = b
Lean

Formalized in Tau Ceti as PeriodPair.exists_g₂_g₃_eq.

Sources
LeanPeriodPair.exists_g₂_g₃_eq
Uses 7
Proof usesA degree-one map is a biholomorphism · Descent of an invariant map to the orbit space · The identity theorem for Riemann surfaces · Rouché's theorem for a disc, classical form · Shimizu's inequality at two cusps · Subgroup.CompactifiedQuotient · TauCeti.ModularGroup.jBiholomorph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.