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

Symmetric Point

defprovedFoundationskey theorem

Documentation

Lean 4 Proof

def symmetricPoint (J : ℕ) (c : ℝ) : Fin J → ℝ := fun _ => c

Dependency Graph

Used by

network_scaling_at_equilibrium network_scaling_normalized unnormCES_symmetricPoint gainsFromVariety_eq_scaling_ratio powerMean_zero network_log_premium SextupleRoleStatement geometricMean_symmetric factorShare_symmetric_uniform detection_asymmetry_bridge diversity_premium_proportional_to_K_logJ network_scaling_linear escort_symmetric_eq_uniform detection_asymmetry network_scaling powerMean_symmetricPoint

Location

thesis/CESProofs/Foundations/Defs.lean:77

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file

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