Documentation

Lean 4 Proof

theorem aggregation_invariance_of_rho (k L : ℕ) (ρ₀ : ℝ) :
    modeAfterL k 2 L ρ₀ = ρ₀ :=
  ces_mode_preserved k L ρ₀

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:33

Module Section

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

In the same file