Sections / Section 2: CES Emergence Theorems / ces_mode_preserved

CES Mode Preserved

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem ces_mode_preserved (k L : ℕ) (a₀ : ℝ) :
    modeAfterL k 2 L a₀ = a₀ := by
  simp [modeAfterL, modeRate, one_pow]

Dependency Graph

Used by

non_ces_decays_relative_to_rho aggregation_invariance_of_rho stability_rho_preserved

Location

thesis/CESProofs/Foundations/Emergence.lean:135

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 mode_geometric_decay modeRate_pos modeRate_lt_one modeRate_in_unit_interval stability_contraction stability_rho_preserved 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