Skip to main content

Module functions

oxilean_std::statistical_learning

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

adaboost_training_error_ty
AdaBoost training error: ≀ exp(-2 Ξ£ Ξ³_tΒ²) after T rounds Type: βˆ€ (T : Nat), Prop
adaboost_ty
AdaBoost: adaptive boosting with exponential loss, T weak learners Type: Nat β†’ Type β†’ Type
app
app2
app3
arrow
backdoor_adjustment_ty
BackdoorAdjustment: P(Y|do(X)) = Ξ£_z P(Y|X,Z=z) P(Z=z) Type: βˆ€ (X Y Z : Type), BackdoorCriterion X Y Z β†’ Prop
backdoor_criterion_ty
BackdoorCriterion: set Z satisfies backdoor criterion for (X, Y) Type: Type β†’ Type β†’ Type β†’ Prop (X, Y, Z β†’ criterion)
bandit_algorithm_ty
BanditAlgorithm: protocol with only loss feedback (no gradient) Type: Nat β†’ Nat β†’ Type (n arms, T rounds)
barron_approximation_ty
BarronApproximation: shallow nets approximate Barron functions at rate 1/√m Type: βˆ€ (B : Real) (m : Nat), Prop (B = norm bound, m = neurons)
barron_space_ty
BarronSpace: functions with finite Barron norm (representable by shallow nets) Type: Real β†’ Type (radius B β†’ function class)
bayesian_regret_bound_ty
BayesianRegretBound: Bayesian regret for Thompson sampling O(√(n T)) Type: βˆ€ (n T : Nat), Prop
benign_overfitting_ty
BenignOverfitting: interpolating solution still generalizes well Type: βˆ€ (n d : Nat), Prop (n samples, d features)
bias_variance_decomposition_ty
Bias-variance decomposition: E[(Ε· - y)Β²] = BiasΒ²(Ε·) + Var(Ε·) + σ² Type: Prop
bias_variance_tradeoff_ty
BiasVarianceTradeoff: MSE = BiasΒ² + Variance + Noise Type: Real β†’ Real β†’ Real β†’ Prop
bool_ty
build_env
Register all statistical learning theory axioms and theorems in the kernel environment.
build_env_extended
Register the extended set of statistical learning theory axioms (Β§7–§17).
bvar
byzantine_fault_tolerance_ty
ByzantineFaultTolerance: learning with f Byzantine clients out of m Type: Nat β†’ Nat β†’ Type (m total, f Byzantine β†’ robust protocol)
calibration_error_ty
CalibrationError: ECE = E[|P(Y=1|score=p) - p|] Type: (List Real) β†’ (List Real) β†’ Real (predictions, labels β†’ ECE)
catoni_pac_bayes_ty
CatoniPACBayes: Catoni’s PAC-Bayes bound with tighter constants Type: βˆ€ (n : Nat) (Ξ΄ : Real), Prop
chain_rule_mi_ty
Chain rule of mutual information: I(X;Y,Z) = I(X;Y) + I(X;Z|Y) Type: Prop
communication_complexity_ty
CommunicationComplexity: total bits communicated to reach Ξ΅ accuracy Type: Real β†’ Nat β†’ Nat (Ξ΅, m β†’ bits)
confounding_bias_ty
ConfoundingBias: bias from ignoring confounders Type: Real β†’ Prop (bias magnitude β†’ bounded)
covariate_shift_ty
CovariateShift: p_S(x) β‰  p_T(x) but p(y|x) the same Type: Type β†’ Prop
cramer_rao_bound_ty
CramΓ©r-Rao bound: Var(ΞΈΜ‚) β‰₯ 1/I(ΞΈ) for any unbiased estimator Type: βˆ€ (p : Real β†’ Real) (ΞΈ : Real), Prop
cst
data_deletion_ty
DataDeletion: privacy-adjacent: model update after removing one point Type: Nat β†’ Real β†’ Type (n, budget β†’ deletion mechanism)
data_dependent_bound_ty
DataDependentBound: a bound that depends on the observed dataset S Type: Nat β†’ Real β†’ Prop (n samples, bound value)
data_processing_inequality_ty
Data processing inequality: I(X;Z) ≀ I(X;Y) for Markov chain Xβ†’Yβ†’Z Type: Prop
depth_separation_ty
DepthSeparation: a function requiring exponentially wide shallow net Type: Nat β†’ Prop (depth d β†’ separation result)
do_calculus_ty
DoCalculus: causal interventional distribution P(Y | do(X=x)) Type: Real β†’ Real β†’ Real (x, context β†’ P(Y | do(X=x)))
domain_adaptation_bound_ty
DomainAdaptationBound: generalization bound under covariate shift Type: βˆ€ (n : Nat) (delta : Real), Prop
domain_adaptation_ty
DomainAdaptation: learning when source and target domains differ Type: Type β†’ Type β†’ Nat β†’ Type (source, target, n β†’ adapted model)
dot_ext
double_descent_ty
DoubleDescent: test error as function of model complexity Type: Nat β†’ Real (n_params β†’ test error curve)
double_rademacher_ty
DoubleRademacher: two-sided Rademacher bound (two-sided uniform convergence) Type: Type β†’ Nat β†’ Real β†’ Prop
dp_generalization_bound_ty
DPGeneralizationBound: utility bound for DP learning Type: βˆ€ (n : Nat) (eps_priv delta_priv : Real), Prop
dp_sample_complexity_ty
DPSampleComplexity: extra samples needed for privacy Type: Real β†’ Real β†’ Real β†’ Real β†’ Nat (Ξ΅_priv, Ξ΄_priv, Ξ΅_learn, Ξ΄_learn β†’ m)
dp_sgd_algorithm_ty
DPSGDAlgorithm: DP-SGD with noise Οƒ, clipping C, epochs T Type: Real β†’ Real β†’ Nat β†’ Type (Οƒ, C, T β†’ algorithm)
early_stopping_reg_ty
EarlyStoppingReg: implicit regularization via iteration count T Type: Nat β†’ Type
elbo_ty
ELBO: evidence lower bound β„’(q) = E_q[log p(x,z)] - E_q[log q(z)] Type: (Real β†’ Real) β†’ (Real β†’ Real) β†’ Real
ewa_algorithm_ty
ExponentialWeightsAlgorithm: EWA (Hedge) distribution over n experts Type: Nat β†’ Real β†’ Type (n experts, learning rate Ξ·)
ewa_regret_bound_ty
EWARegretBound: R_T(EWA) ≀ ln(n)/Ξ· + Ξ· T/2 Type: βˆ€ (n : Nat) (T : Nat) (Ξ· : Real), Prop
feature_map_ty
FeatureMap: Ο†: X β†’ H_k with k(x,x’) = βŸ¨Ο†(x),Ο†(x’)⟩ Type: Type β†’ Type β†’ Type
fedavg_convergence_ty
FedAvgConvergence: FedAvg converges at rate O(1/√(T m)) Type: βˆ€ (T m : Nat), Prop
federated_learning_ty
FederatedLearning: distributed optimization across m clients Type: Nat β†’ Nat β†’ Type (m clients, T rounds β†’ protocol)
fisher_information_ty
FisherInformation: I(ΞΈ) = E[(βˆ‚/βˆ‚ΞΈ log p(x;ΞΈ))Β²] Type: (Real β†’ Real) β†’ Real β†’ Real
fundamental_theorem_pac_ty
Fundamental theorem of PAC learning: finite VC dimension ↔ PAC learnability Type: βˆ€ (H : Type), VCDimension H < ∞ β†’ PACLearnability H
gaussian_complexity_ty
GaussianComplexity: G_n(H) = E_{g,S}[sup_{h∈H} (1/n) Ξ£ g_i h(x_i)] Type: Type β†’ Nat β†’ Real
growth_function_ty
GrowthFunction: Ξ _H(m) = max_{S,|S|=m} |{h|_S : h ∈ H}| Type: Type β†’ Nat β†’ Nat
heterogeneity_measure_ty
HeterogeneityMeasure: degree of statistical heterogeneity across clients Type: Nat β†’ Real β†’ Prop (m clients, Ξ“ measure β†’ bound)
implicit_regularization_ty
ImplicitRegularization: GD with zero init converges to min-norm solution Type: Nat β†’ Real β†’ Prop (steps T, step size Ξ·)
importance_weighting_ty
ImportanceWeighting: reweight source samples by p_T(x)/p_S(x) Type: (Real β†’ Real) β†’ (Real β†’ Real) β†’ Real β†’ Real (p_T, p_S, x β†’ weight)
interventional_dist_ty
InterventionalDist: P(Y | do(X)) in a structural causal model Type: Type β†’ Type β†’ Type (X space, Y space β†’ dist)
kernel_function_ty
KernelFunction: k: X Γ— X β†’ ℝ, a positive-definite symmetric function Type: Type β†’ Type (representing a kernel on X)
kernel_matrix_ty
KernelMatrix: Gram matrix K_{ij} = k(x_i, x_j) ∈ ℝ^{nΓ—n} Type: (Type β†’ Type) β†’ Nat β†’ Type
kernel_pca_projection_ty
KernelPCAProjection: projection onto top-k kernel PCA components Type: (Type β†’ Type) β†’ Nat β†’ Nat β†’ Type (kernel, n, k β†’ projector)
kernel_pca_ty
Kernel PCA: principal components in feature space via eigendecomposition of K Type: (Type β†’ Type) β†’ Nat β†’ Nat β†’ Type
kernel_svm_ty
KernelSVM: support vector machine with kernel trick Type: (Type β†’ Type) β†’ Real β†’ Type
lasso_reg_ty
LassoReg: ℓ₁ regularization Ξ»β€–h‖₁ (sparsity-promoting) Type: Real β†’ Type
list_ty
localized_bound_ty
LocalizedBound: generalization bound via localized Rademacher Type: βˆ€ (H : Type) (n : Nat) (Ξ΄ : Real), Prop
localized_rademacher_ty
LocalizedRademacher: local Rademacher complexity around minimizer Type: Type β†’ Nat β†’ Real β†’ Real (H, n, radius β†’ complexity)
mercer_theorem_ty
Mercer’s theorem: k is p.d. ↔ βˆƒ feature map Ο† with k(x,x’) = βŸ¨Ο†(x),Ο†(x’)⟩ Type: βˆ€ (k : Type β†’ Type), isPositiveDefinite k ↔ βˆƒ feature map, Prop
min_norm_interpolation_ty
MinNormInterpolation: min-β€–wβ€– solution that fits training data exactly Type: Nat β†’ Nat β†’ Type (n samples, d features β†’ solution)
ml_kl_divergence_ty
MLKLDivergence: D_KL(Pβ€–Q) = Ξ£ P log(P/Q) β€” used in PAC-Bayes bounds Type: (List Real) β†’ (List Real) β†’ Real
ml_mutual_information_ty
MLMutualInformation: I(X;Y) = H(X) - H(X|Y) for learning-theoretic analysis Type: (List Real) β†’ (List Real) β†’ Real
multiplicative_weights_update_ty
MultiplicativeWeightsUpdate: MW update step at round t Type: Nat β†’ Real β†’ Type (n, Ξ·)
nat_ty
neural_network_ty
NeuralNetwork: a feedforward network of given depth and width Type: Nat β†’ Nat β†’ Type (depth, width β†’ network)
nn_expressivity_ty
NNExpressivity: VC dimension / capacity of a neural net class Type: Nat β†’ Nat β†’ Nat (depth, width β†’ VC dim)
nn_generalization_bound_ty
NNGeneralizationBound: Rademacher-based bound for neural networks Type: βˆ€ (depth width n : Nat) (Ξ΄ : Real), Prop
ogd_regret_bound_ty
OGD regret bound: R_T ≀ DΒ²/(2Ξ·) + Ξ· Ξ£β€–βˆ‡_tβ€–Β² ≀ DΒ·G·√(2T) Type: βˆ€ (T : Nat) (eta : Real), Prop
on_average_stability_ty
OnAverageStability: E_S[E_z|L(A(S),z) - L(A(S^{(i)}),z)|] ≀ Ξ² Type: Real β†’ Prop
online_algorithm_ty
OnlineAlgorithm: sequential prediction protocol over T rounds Type: Nat β†’ Type
online_gradient_descent_ty
OnlineGradientDescent: OGD with regret O(√T) Type: Real β†’ Nat β†’ Type (learning rate Ξ·, rounds T)
pac_bayes_bound_ty
PAC-Bayes bound: L_D(Q) ≀ L_S(Q) + √((D_KL(Qβ€–P) + log(n/Ξ΄))/(2n)) Type: βˆ€ (n : Nat) (Ξ΄ : Real), Prop
pac_bayes_mcallester_ty
PACBayesBound: McAllester’s PAC-Bayes bound Type: βˆ€ (n : Nat) (Ξ΄ : Real), (List Real) β†’ (List Real) β†’ Prop
pac_learnability_ty
PACLearnability: a hypothesis class is PAC learnable Type: Type β†’ Prop
pac_learner_ty
PACLearner: a learning algorithm that for any Ξ΅, Ξ΄ > 0 returns h with L_D(h) ≀ Ξ΅ Type: Real β†’ Real β†’ Nat β†’ Type
perceptron_mistake_bound_ty
Perceptron mistake bound: M ≀ (R/Ξ³)Β² where R = maxβ€–xβ€–, Ξ³ = margin Type: βˆ€ (R Ξ³ : Real), mistakes ≀ (R/Ξ³)Β²
perceptron_ty
Perceptron: online linear classifier with mistake bound Type: Nat β†’ Type (dimension β†’ perceptron)
pi
private_pac_learning_ty
PrivatePACLearning: PAC learning with (Ξ΅, Ξ΄)-differential privacy Type: Real β†’ Real β†’ Type (Ξ΅_priv, Ξ΄_priv β†’ learner)
private_query_mechanism_ty
PrivateQueryMechanism: answering statistical queries with DP Type: Real β†’ Real β†’ Type (Ξ΅, Ξ΄ β†’ mechanism)
prop
proper_scoring_rule_ty
ProperScoringRule: S(f, y) is proper if E[S(f,Y)] maximized by true dist Type: (Real β†’ Real) β†’ Real β†’ Real (forecast function, outcome β†’ score)
rademacher_bound_ty
Rademacher generalization bound: L_D(h) ≀ L_S(h) + 2 R_n(H) + O(√(log(1/Ξ΄)/n)) Type: βˆ€ (H : Type) (n : Nat) (Ξ΄ : Real), Prop
rademacher_complexity_ty
RademacherComplexity: R_n(H) = E_{Οƒ,S}[sup_{h∈H} (1/n) Ξ£ Οƒ_i h(x_i)] Type: Type β†’ Nat β†’ Real
real_ty
regret_bound_ty
RegretBound: R_T = Ξ£ L_t(h_t) - min_h Ξ£ L_t(h) ≀ O(√T) Type: Nat β†’ Real β†’ Prop (rounds T, bound Ξ΅)
regularized_objective_ty
RegularizedObjective: L(h) + Ξ» Ξ©(h) Type: Real β†’ Type (regularization weight β†’ regularized problem)
reliability_diagram_ty
ReliabilityDiagram: calibration curve P(Y=1 | score ∈ bin) vs. score Type: Nat β†’ Type (n bins β†’ diagram)
representer_theorem_ty
Representer theorem: optimal solution in RKHS lies in span of kernel evaluations Type: βˆ€ (k : Type β†’ Type) (n : Nat), Prop
ridge_regression_solution_ty
Ridge regression solution: (X^T X + Ξ»I)^{-1} X^T y Type: βˆ€ (n d : Nat) (Ξ» : Real), List (List Real) β†’ List Real β†’ List Real
rkhs_norm_ty
RKHSNorm: β€–fβ€–{H_k}Β² = Ξ£{i,j} Ξ±_i Ξ±_j k(x_i, x_j) Type: (Type β†’ Type) β†’ Real (kernel β†’ normΒ²)
rkhs_ty
RKHS: reproducing kernel Hilbert space H_k associated to kernel k Type: (Type β†’ Type) β†’ Type
sample_complexity_bound_ty
Sample complexity upper bound for PAC learning Type: βˆ€ (Ξ΅ Ξ΄ : Real) (d : Nat), m β‰₯ SampleComplexity Ξ΅ Ξ΄ d β†’ Prop
sample_complexity_ty
SampleComplexity: m = O((d log(d/Ξ΅) + log(1/Ξ΄)) / Ξ΅) Type: Real β†’ Real β†’ Nat β†’ Nat
sauer_shelah_ty
Sauer-Shelah lemma: Ξ _H(m) ≀ Ξ£_{i=0}^{d} C(m,i) Type: βˆ€ (H : Type) (m : Nat), GrowthFunction H m ≀ Sauer_bound (VCDimension H) m
sharpness_measure_ty
SharpnessMeasure: variance of the forecast distribution Type: (List Real) β†’ Real (forecasts β†’ sharpness)
stability_generalization_bound_ty
StabilityGeneralizationBound: Ξ²-stable β†’ gen error ≀ 2Ξ² + O(1/√n) Type: βˆ€ (Ξ² : Real) (n : Nat) (Ξ΄ : Real), Prop
svm_generalization_bound_ty
SVMGeneralizationBound: margin-based bound ≀ RΒ²/(Ξ³Β² n) Type: βˆ€ (n : Nat) (R Ξ³ : Real), Prop
symmetrization_lemma_ty
Symmetrization lemma: relates population risk to Rademacher complexity Type: βˆ€ (H : Type) (n : Nat), Prop
thompson_sampling_ty
ThompsonSampling: Bayesian bandit via posterior sampling Type: Nat β†’ Type (n arms)
tikhonov_reg_ty
TikhonovReg: Tikhonov regularization Ξ»β€–hβ€–Β²_{H_k} Type: Real β†’ (Type β†’ Type) β†’ Type
type0
ucb_algorithm_ty
UCBAlgorithm: upper confidence bound algorithm Type: Nat β†’ Real β†’ Type (n arms, exploration param c)
ucb_regret_bound_ty
UCBRegretBound: UCB1 regret O(√(n T ln T)) Type: βˆ€ (n T : Nat), Prop
uniform_convergence_ty
UniformConvergence: sup_{h∈H} |L_D(h) - L_S(h)| ≀ Ξ΅ w.p. β‰₯ 1βˆ’Ξ΄ Type: Type β†’ Real β†’ Real β†’ Prop
uniform_stability_ty
UniformStability: |L(A(S), z) - L(A(S’), z)| ≀ Ξ² for any S, S’ differing in 1 point Type: Real β†’ Prop (Ξ² β†’ stability predicate)
vc_dimension_ty
VCDimension: maximal shattered set size for a hypothesis class H Type: Type β†’ Nat