Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.weighted-estimators

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/weighted_estimators.clj5 definitions, 5 theorems

Kochenderfer weighted-sum / additive estimators (across Optimization and Validation) as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: V7.4 multiple importance sampling : balance-weighted combination of proposals V11.3 integrated gradients : path-sum attribution (completeness: sum = delta) O6.4 Gauss-Newton Hessian : sum of squared Jacobian terms O17.6 ridge regression : data loss + lambda * penalty O21.5 Bayesian Monte Carlo : quadrature-weighted mean MIS reuses nnrat/wsum2 and inherits the convex bound (estimate <= max proposal when balance weights sum to one). The rest are add/multiply compositions with worked instances. Native and axiom-free; chains nnrat-convex (-> wsum2, minmax) on d63.

Depends onmath.rational.nnrat.convex

est/mis-combine :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

xai/ig-attribution-total :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

opt/gauss-newton-hessian :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

opt/ridge-objective :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

est/bayesian-mc-mean :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

est/mis-within-max :
  (w0 w1 f0 f1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → eda/pipe-update w0 w1 f0 f1 ≤ minmax/max f0 f1

xai/ig-completeness-example :
  → astar/f-value 1/2 1/2 = 1

opt/gauss-newton-example :
  → opt/gauss-newton-hessian 1 2 = 5

opt/ridge-example :
  → sac/soft-value 1/2 1 1/2 = 1

est/bayesian-mc-example :
  → eda/pipe-update 1/2 1/2 1 0 = 1/2