Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app

app2

app3

arrow

azuma_hoeffding_ty

AzumaHoeffding : Prop — P(M_n - M_0 ≥ t) ≤ exp(-t²/(2Σc_i²)) for a bounded-difference martingale.

azuma_inequality_ty

AzumaInequality : Prop — Azuma’s inequality for martingale difference sequences with bounded differences.

bayes_theorem_ty

BayesTheorem : Prop — P(A|B) = P(B|A) * P(A) / P(B).

bayes_update

Computes the posterior distribution via Bayes’ theorem.

bernstein_inequality_ty

BernsteinInequality : Prop — a refined concentration bound exploiting variance information.

berry_esseen_ty

BerryEsseenBound : Prop — |F_n(x) - Φ(x)| ≤ C ρ / (σ³ √n) uniformly in x.

beta_pdf

Approximates the beta PDF: f(x; α, β) for x ∈ (0, 1).

binomial_coeff

binomial_pmf

Computes the binomial PMF: P(X = k) for X ~ Bin(n, p).

branching_process_ty

BranchingProcess : (Nat → Distribution) → (Nat → Nat) → Prop — a Galton–Watson branching process with offspring distribution Z_n.

brownian_motion_ty

BrownianMotion : (Real → Ω → Real) → Prop — a stochastic process W satisfying: W(0)=0, independent increments, Gaussian increments W(t)-W(s) ~ N(0, t-s), and continuous paths.

build_advanced_probability_env

Extends the environment built by build_probability_env with the advanced axioms from Section 9.

build_probability_env

Register all probability theory axioms and type declarations into env.

bvar

central_limit_theorem_ty

CentralLimitTheorem : Prop — normalized sums converge in distribution to the standard normal.

characteristic_fn_ty

CharacteristicFn : (Ω → Real) → Real → Complex — the characteristic function φ_X(t) = E[exp(itX)] of a random variable.

chebyshev_inequality_ty

ChebyshevInequality : Prop — P(|X - μ| ≥ k·σ) ≤ 1/k² for k > 0.

chernoff_bound_ty

ChernoffBound : Prop — tail bound via the moment generating function: P(X ≥ t) ≤ e^{-st} M_X(s).

conditional_expectation_ty

ConditionalExpectation : (Ω → Real) → SigmaAlgebra Ω → (Ω → Real) — the conditional expectation E[X | F] as a measurable function.

continuum_random_tree_ty

ContinuumRandomTree : Type — the Brownian continuum random tree (CRT) as the scaling limit.

coupling_lemma_ty

CouplingLemma : Prop — d_TV(P, Q) = inf_{coupling} P(X ≠ Y) over all couplings of P and Q.

coupling_ty

Coupling : Distribution α → Distribution α → Type — a coupling of two distributions (a joint distribution with given marginals).

covariance

Computes the sample covariance of paired slices x and y.

covariance_ty

Covariance : (Ω → Real) → (Ω → Real) → Real — the covariance E[(X - EX)(Y - EY)] of two random variables.

cramer_ldp_ty

CramerLDP : Prop — the Cramér large deviation principle for i.i.d. sums.

crp_ty

CRP : Real → Nat → Distribution — the Chinese Restaurant Process: CRP(α, n) gives distribution over partitions of [n].

cst

d_separation_ty

DSeparation : (Nat → Nat → Prop) → Nat → Nat → (Nat → Prop) → Prop — d-separation in a DAG: u ⊥ v | Z given separating set Z.

dirichlet_process_ty

DirichletProcess : Real → Distribution → Distribution — the Dirichlet process DP(α, G₀) with concentration α and base measure G₀.

discrete_uniform

Returns the uniform distribution over n outcomes: each probability is 1/n.

distribution_ty

Distribution : Type → Type — a probability measure (distribution) on a type.

donsker_thm_ty

DonskerThm : Prop — Donsker’s functional CLT: the empirical process converges to Brownian bridge.

doob_optional_sampling_ty

DoobOptionalSampling : Prop — E[M_τ] = E[M_0] for a uniformly integrable martingale stopped at τ.

empirical_measure_ty

EmpiricalMeasure : Nat → (Nat → α) → Distribution α — the empirical measure L_n = (1/n) Σ δ_{X_i}.

empirical_moments

Computes empirical moments up to order max_order from data.

entropy_ty

Entropy : Distribution α → Real — the Shannon entropy H(X) = -∑ p(x) log p(x).

event_ty

Event : Type → Prop — an event as a measurable subset of the sample space.

exponential_cdf

Computes the exponential CDF: F(x; λ) = 1 - exp(-λx) for x ≥ 0.

exponential_pdf

Computes the exponential PDF: f(x; λ) = λ exp(-λx) for x ≥ 0.

extinction_prob_ty

ExtinctionProbability : BranchingProcess → Real — the probability q = P(eventual extinction) for a branching process.

factorial

faithfulness_ty

Faithfulness : (Nat → Nat → Prop) → Distribution → Prop — the faithfulness condition: every conditional independence in P is entailed by the graph.

fenchel_legendre_ty

FenchelLegendre : (Real → Real) → (Real → Real) — the Fenchel–Legendre transform I(x) = sup_λ (λx - Λ(λ)).

fisher_tippett_gnedenko_ty

FisherTippettGnedenko : Prop — the Fisher–Tippett–Gnedenko theorem: block maxima converge to a GEV distribution.

free_convolution_ty

FreeConvolution : Distribution → Distribution → Distribution — the free additive convolution ⊞ of two spectral distributions.

free_independence_ty

FreeIndependence : FreeProbabilitySpace → FreeProbabilitySpace → Prop — freeness (free independence) in the sense of Voiculescu.

free_probability_space_ty

FreeProbabilitySpace : Type — a non-commutative probability space (A, φ) for free probability theory.

gamma_pdf

Approximates the gamma PDF: f(x; α, β) using the log-gamma function.

gartner_ellis_ty

GartnerEllis : Prop — the Gärtner–Ellis theorem: LDP from the limit of (1/n) log E[e^{nλX_n}].

gaussian_process_ty

GaussianProcess : ((Ω → Real) → (Ω → Real) → Real) → Prop — a stochastic process GP(m, k) fully specified by mean m and covariance kernel k.

geometric_pmf

Computes the geometric PMF: P(X = k) = (1-p)^(k-1) p for k ≥ 1.

gev_distribution_ty

GEVDistribution : Real → Real → Real → Type — the generalised extreme value distribution GEV(μ, σ, ξ).

girsanov_thm_ty

GirsanovThm : Prop — Girsanov’s theorem: change of measure via Novikov’s condition, W̃_t = W_t - ∫θ_s ds is Brownian under ℚ.

gpd_distribution_ty

GPDDistribution : Real → Real → Type — the generalised Pareto distribution GPD(σ, ξ) for peaks over threshold.

green_function_ty

GreenFunction : MarkovChain → Nat → Nat → Real — the expected number of visits to state j starting from i: G(i,j) = Σ_{t≥0} P^t(i,j).

hitting_time_ty

HittingTime : MarkovChain → Nat → (Ω → Nat) — the first passage time τ_j = min{t ≥ 1 : X_t = j}.

hoeffding_inequality_ty

HoeffdingInequality : Prop — P(S_n - E[S_n] ≥ t) ≤ exp(-2t²/Σ(b_i-a_i)²) for bounded summands.

ito_formula_ty

ItoFormula : Prop — Itô’s lemma: df(t, X_t) = ∂_t f dt + ∂_x f dX + ½ ∂_xx f d⟨X⟩.

ito_integral_ty

ItoIntegral : (Real → Ω → Real) → (Real → Ω → Real) → (Ω → Real) — the Itô stochastic integral ∫H dW for an adapted integrand H and Brownian W.

kl_divergence

Computes the KL divergence D_KL(p ‖ q) = Σ p_i log(p_i / q_i).

kl_divergence_ty

KLDivergence : Distribution α → Distribution α → Real — the Kullback–Leibler divergence D_KL(P ‖ Q).

kolmogorov_axioms_ty

KolmogorovAxioms : Prop — the three Kolmogorov axioms for a probability measure.

law_of_large_numbers_ty

OriginalLawOfLargeNumbers : Prop — the sample mean converges to the population mean.

ldp_ty

LDP : Distribution → (Real → Real) → Prop — the large deviation principle: lim(1/n) log P(S_n/n ∈ A) = -inf_{x∈A} I(x).

levy_process_ty

LevyProcess : (Real → Ω → Real) → Prop — a process with stationary independent increments, càdlàg paths, X(0)=0.

lindeberg_clt_ty

LindebergCLT : Prop — the CLT under the Lindeberg condition (triangular arrays).

log_gamma

Stirling approximation of log Γ(x) for x > 0.

log_mgf_ty

LogMGF : (Ω → Real) → Real → Real — the log moment generating function Λ(λ) = log E[e^{λX}].

lyapunov_clt_ty

LyapunovCLT : Prop — the CLT under the Lyapunov condition (finite 2+δ moments).

markov_blanket_ty

MarkovBlanket : (Nat → Prop) → Nat → Nat → Prop — node v is in the Markov blanket of u in graph G: conditional independence given blanket.

markov_chain_ty

MarkovChain : Type → Type — a discrete-time Markov chain on a state space.

markov_inequality_ty

MarkovInequality : Prop — P(X ≥ a) ≤ E[X] / a for non-negative X and a > 0.

martingale_ty

Martingale : StochasticProcess → Prop — a stochastic process M is a martingale: E[M_{n+1} | F_n] = M_n.

mcdiarmid_inequality_ty

McDiarmidInequality : Prop — if f(x_1,…,x_n) changes by at most c_i when x_i is replaced, then P(f - Ef ≥ t) ≤ exp(-2t²/Σc_i²).

measurable_ty

Measurable : (α → β) → SigmaAlgebra α → SigmaAlgebra β → Prop — a function is measurable with respect to given sigma-algebras.

mixing_time_ty

MixingTime : MarkovChain α → Real → Nat — the ε-mixing time of a Markov chain.

mutual_independence_ty

MutualIndependence : List Event → Prop — a family of events is mutually independent.

nat_ty

negative_binomial_pmf

Computes the negative binomial PMF: P(X = k) for X ~ NB(r, p).

normal_pdf

Computes the Gaussian (normal) PDF: f(x; μ, σ).

pairwise_independence_ty

PairwiseIndependence : List Event → Prop — every pair of events in a family is independent.

pearson_correlation

Computes the Pearson correlation coefficient between x and y.

pi

pickands_balkema_de_haan_ty

PickandsBalkemaDeHaan : Prop — the Pickands–Balkema–de Haan theorem: exceedances over high threshold converge to a GPD.

poisson_pmf

Computes the Poisson PMF: P(X = k) for X ~ Pois(λ).

prob_measure_ty

ProbMeasure : SigmaAlgebra α → Type — a probability measure on a measurable space.

prob_space_ty

ProbSpace : Type — a probability space Ω equipped with a sigma-algebra and measure.

prop

quadratic_variation_ty

QuadraticVariation : (Real → Ω → Real) → (Ω → Real) → Prop — the quadratic variation ⟨X⟩_T of a semimartingale X.

quantile_ty

Quantile : Distribution α → Real → α — the quantile function (inverse CDF) of a distribution.

quantum_prob_space_ty

QuantumProbSpace : Type — a quantum probability space given by a C*-algebra A with state φ.

rademacher_complexity_ty

RademacherComplexity : ((Ω → Real) → Prop) → Real → Real — the Rademacher complexity of a function class F over n samples.

random_tree_ty

RandomTree : Nat → Type — a random recursive tree (or Galton–Watson tree) with n nodes.

random_var_ty

RandomVar : Type → Type → Type — a measurable function from sample space to value space.

random_walk_ty

RandomWalk : (Nat → Ω → Real) → Prop — a random walk S_n = X_1 + ⋯ + X_n with i.i.d. steps X_i.

rate_function_ty

RateFunction : Distribution α → (α → Real) → Prop — the large-deviation rate function I satisfying the LDP.

real_ty

renewal_process_ty

RenewalProcess : (Nat → Real) → Prop — the inter-arrival times form a renewal process.

renewal_reward_ty

RenewalReward : Prop — the renewal reward theorem: long-run average reward = E[reward]/E[inter-arrival].

reversible_chain_ty

ReversibleChain : MarkovChain → Distribution → Prop — detailed balance: π(i) P(i,j) = π(j) P(j,i) for all states i, j.

sample_mean

Computes the sample mean of data.

sample_variance

Computes the sample variance of data (unbiased, divides by n-1).

sanov_ldp_ty

SanovLDP : Prop — the Sanov large deviation principle for empirical measures.

sde_ty

SDE : (Real → Ω → Real) → (Real → Real → Real) → (Real → Real → Real) → Prop — the stochastic differential equation dX = μ(t,X)dt + σ(t,X)dW.

sigma_algebra_ty

SigmaAlgebra : Type → Type — a sigma-algebra F on a sample space Ω. Satisfies closure under complement and countable union.

spectral_gap_ty

SpectralGap : MarkovChain → Real — the spectral gap 1 - λ_2 of the transition matrix (λ_2 = second largest eigenvalue).

standard_normal_cdf

Approximates the standard normal CDF Φ(z) for z ∈ ℝ.

stochastic_process_ty

StochasticProcess : Nat → Type → Type — a time-indexed family of random variables.

stopping_time_ty

StoppingTime : (Nat → Event) → Prop — a random time τ adapted to a filtration is a stopping time.

strong_lln_ty

StrongLawOfLargeNumbers : Prop — the sample mean converges almost surely to the population mean.

strong_solution_ty

StrongSolution : SDE → Prop — the SDE has a strong solution (pathwise unique, adapted to W’s filtration).

sub_exponential_ty

SubExponential : (Ω → Real) → Real → Real → Prop — X is (σ², b)-sub-exponential.

sub_gaussian_ty

SubGaussian : (Ω → Real) → Real → Prop — X is σ-sub-Gaussian: E[exp(λX)] ≤ exp(λ²σ²/2) for all λ.

total_variation_dist_ty

TotalVariationDist : Distribution α → Distribution α → Real — the total variation distance between two probability measures.

total_variation_distance

Computes the total variation distance between two discrete distributions.

type0

vc_dimension_ty

VCDimension : ((Ω → Prop) → Prop) → Nat — the Vapnik–Chervonenkis dimension of a hypothesis class H.

weak_lln_ty

WeakLawOfLargeNumbers : Prop — the sample mean converges in probability to the population mean.

weak_solution_ty

WeakSolution : SDE → Prop — the SDE has a weak solution (exists on some probability space).