Sections / Section 1: CES Definition and Basic Properties / AggFun

Agg Function

defprovedFoundations

Documentation

Lean 4 Proof

def AggFun (J : ℕ) := (Fin J → ℝ) → ℝ

Dependency Graph

Used by

EquivalenceStatement IsContinuousAgg aczel subadditivity_qualitative emergent_CES IsHomogDegOne aggregationOp powerMean quasiArithMean ces_equivalence weighted_emergence superadditivity_qualitative IsSymmetric IsQuasiArithMean anova_mode_connection IsScaleConsistent manipulationPayoff superadditivity_quantitative_bound IsAggFixedPoint IsPowerMean kolmogorov_nagumo IsHomogDeg aggregation_fixed_point IsStrictlyIncreasing

Location

thesis/CESProofs/Foundations/Defs.lean:22

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file

QAGenerator quasiArithMean powerMean cesFun unnormCES irsCES curvatureKH curvatureK curvatureK_eq_curvatureKH symmetricPoint IsSymmetric IsStrictlyIncreasing IsHomogDegOne IsHomogDeg IsScaleConsistent IsContinuousAgg IsQuasiArithMean IsPowerMean powerMean_symmetricPoint curvatureK_pos