Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

analytic_continuation_ty

Analytic continuation: two entire functions agreeing on an open set agree everywhere

app

app2

app3

argument_principle_ty

Argument principle: (1/2πi)∮ f’/f dz = Z - P (zeros minus poles)

arrow

bloch_theorem_ty

Bloch’s theorem: image of unit disk contains a disk of radius B (Bloch’s constant)

bohr_theorem_ty

Bohr’s theorem: |f| < 1 on disk ⟹ power series converges in disk of radius 1/3

build_complex_env

Build the complex number environment, registering all axioms and theorems.

bvar

cauchy_integral_approx

Cauchy integral formula computation (simple approximation).

cauchy_integral_formula_ty

Cauchy integral formula: f(z₀) = (1/2πi) ∮ f(z)/(z-z₀) dz

cauchy_integral_theorem_ty

Cauchy’s integral theorem: ∮_C f(z) dz = 0 for holomorphic f and closed curve C

cauchy_riemann_ty

CauchyRiemann: holomorphicity ↔ Cauchy-Riemann equations ∀ f : ℂ → ℂ, IsHolomorphic f ↔ SatisfiesCauchyRiemann f

complex_abs_ty

Complex.abs : Complex → Real (|z| = √(re² + im²))

complex_add_ty

Complex.add : Complex → Complex → Complex

complex_arg_ty

Complex.arg : Complex → Real (argument, in (-π, π])

complex_conj_ty

Complex.conj : Complex → Complex (complex conjugate: a + bi → a - bi)

complex_exp_ty

Complex.exp : Complex → Complex (complex exponential)

complex_i_ty

Complex.I : Complex (imaginary unit i = (0, 1))

complex_im_ty

Complex.im : Complex → Real

complex_log_ty

Complex.log : Complex → Complex (principal value logarithm)

complex_mk_ty

Complex.mk : Real → Real → Complex

complex_mul_ty

Complex.mul : Complex → Complex → Complex

complex_neg_ty

Complex.neg : Complex → Complex

complex_norm_sq_ty

Complex.normSq : Complex → Real (|z|² = re² + im²)

complex_of_real_ty

Complex.ofReal : Real → Complex (coercion ℝ → ℂ)

complex_pow_ty

Complex.pow : Complex → Nat → Complex

complex_re_ty

Complex.re : Complex → Real

complex_sqrt_ty

Complex.sqrt : Complex → Complex (principal square root)

complex_ty

complex_type_decl

Complex : Type (ℂ = ℝ × ℝ as a structure)

contour_integrate_circular

Numerically integrate f along a circular contour centered at center with given radius. Uses n_points equally spaced quadrature nodes (trapezoidal rule on the circle). Returns the integral ∮ f(z) dz (NOT divided by 2πi).

cst

de_moivre_theorem_ty

De Moivre’s theorem: (cos θ + i·sin θ)^n = cos(n·θ) + i·sin(n·θ)

dft

Discrete Fourier Transform: X[k] = Σ_{n=0}^{N-1} x[n] · e^(-2πi·k·n/N).

elliptic_liouville_ty

Liouville theorem for elliptic functions: bounded implies constant

euler_formula_ty

Euler’s formula: exp(i·θ) = cos(θ) + i·sin(θ)

fft

Cooley-Tukey radix-2 FFT (N must be a power of two; falls back to DFT otherwise).

fundamental_theorem_algebra_ty

Fundamental theorem of algebra: every non-constant polynomial over ℂ has a root

hadamard_factorization_ty

Hadamard factorization theorem: entire function of finite order has Weierstrass product form

hardy_banach_ty

Hardy space H^p is a Banach space for p ≥ 1

hartogs_theorem_ty

Hartogs’ theorem: holomorphic functions in several variables extend across compact singularities

idft

Inverse Discrete Fourier Transform: x[n] = (1/N) Σ_{k=0}^{N-1} X[k] · e^(2πi·k·n/N).

impl_pi

jensen_formula_ty

Jensen’s formula: log|f(0)| = Σ log(r/|zₖ|) + (1/2π)∫₀²π log|f(re^{iθ})| dθ

laurent_series_ty

Laurent series convergence: every meromorphic function has a Laurent series in an annulus

liouville_theorem_ty

Liouville’s theorem: every bounded entire function is constant

mandelbrot_ascii

Render a simple ASCII Mandelbrot set for a given rectangular region. Returns a Vec<String> with one row per line.

mandelbrot_iter

Check membership in the Mandelbrot set: iterate z ↦ z² + c from z = 0. Returns None if c is in the set (within max_iter), or Some(escape_iter).

meromorphic_riemann_sphere_ty

Meromorphic function on the Riemann sphere is a rational function

mittag_leffler_theorem_ty

Mittag-Leffler theorem: meromorphic function with prescribed poles exists

mobius_conformal_ty

Every Möbius transformation is a conformal automorphism of the Riemann sphere

mobius_group_ty

Möbius transformations form a group (PSL(2,ℂ))

modular_form_finite_dim_ty

The space of modular forms of weight k is finite-dimensional

nat_ty

nevanlinna_first_theorem_ty

Nevanlinna’s first fundamental theorem: T(r, f) = m(r, f) + N(r, f) + O(1)

nevanlinna_second_theorem_ty

Nevanlinna’s second fundamental theorem: sum of Nevanlinna deficiencies ≤ 2

newton_method

Newton’s method for finding a root of f (with derivative df), starting at z0. Returns Some(root) if converged within max_iter iterations to within tol.

oka_theorem_ty

Oka’s theorem: pseudoconvex ↔ domain of holomorphy in ℂⁿ

paley_wiener_theorem_ty

Paley-Wiener: L² function is bandlimited ↔ Fourier transform has compact support

phragmen_lindelof_ty

Phragmén-Lindelöf: maximum modulus principle extended to unbounded sectors

pi

picard_great_theorem_ty

Picard’s great theorem: near an essential singularity, f is densely surjective (minus at most one point)

picard_little_theorem_ty

Picard’s little theorem: a non-constant entire function omits at most one value

prop

real_ty

residue_theorem_ty

Residue theorem: ∮_C f dz = 2πi · Σ Res(f, zₖ)

riemann_hypothesis_ty

Riemann hypothesis (as axiom): non-trivial zeros of ζ lie on Re(s) = 1/2

riemann_mapping_theorem_ty

Riemann mapping theorem: every simply connected proper open subset of ℂ is conformally equivalent to the disk

riemann_zeta_approx

Approximate the Riemann zeta function ζ(s) via the first n_terms of the Dirichlet series. Converges for Re(s) > 1; use n_terms ≥ 1000 for reasonable accuracy.

riemann_zeta_euler_product

Euler product approximation of ζ(s): ∏_{p prime} 1/(1 - p^{-s}) over the first n_primes primes.

riemann_zeta_meromorphic_ty

Riemann zeta function extends meromorphically to ℂ with a simple pole at s = 1

roots_of_unity_ty

n-th roots of unity: z^n = 1 has exactly n solutions in ℂ

rouche_theorem_ty

Rouché’s theorem: if |f| > |g| on C, then f and f+g have the same number of zeros inside C

runge_theorem_ty

Runge’s theorem: holomorphic functions on a compact set can be approximated by rational functions

schwarz_pick_lemma_ty

Schwarz-Pick lemma: holomorphic self-map of the unit disk is a hyperbolic contraction

sieve_of_eratosthenes

Sieve of Eratosthenes: returns the first count prime numbers.

type0

weierstrass_factorization_ty

Weierstrass factorization theorem: every entire function factors via its zero set

weierstrass_p_ty

Weierstrass ℘-function is an elliptic function for its lattice