Rho Mode Rate Is One

theorem proved Foundations

Documentation

Lean 4 Proof

theorem rho_mode_rate_is_one (k : ℕ) :
    modeRate k 2 = 1 := by
  simp [modeRate]

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:40

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file

aggregation_invariance_of_rho non_ces_decays_relative_to_rho rho_renyi_correspondence_support uniform_collision_probability effectiveCESPotential tail_powerlaw tail_compact tail_exponential_at_q_one basin_of_attraction_structure basin_is_global convergence_rate_cubic