Sections / Section 2: CES Emergence Theorems / stability_rho_preserved

Stability Rho Preserved

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem stability_rho_preserved (k L : ℕ) (a₀ : ℝ) :
    modeAfterL k 2 L a₀ = a₀ :=
  ces_mode_preserved k L a₀

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:197

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file

aggregationOp IsAggFixedPoint aggregation_fixed_point powerMean_zero powerMean_isFixedPoint modeRate modeAfterL ces_mode_preserved mode_geometric_decay modeRate_pos modeRate_lt_one modeRate_in_unit_interval stability_contraction stability_mode_contraction anova_mode_connection sum_sq_ge_inv_card collision_entropy_le_log_J power_sum_bound_concave power_sum_bound_convex power_sum_pos