Documentation

Lean 4 Proof

theorem non_ces_decays_relative_to_rho {k : ℕ} (_hk : 2 ≤ k) {m : ℕ} (_hm : 3 ≤ m)
    (L : ℕ) (a_ces a_nonCES : ℝ) (_ha : a_nonCES ≠ 0) :
    |modeAfterL k m L a_nonCES| / |modeAfterL k 2 L a_ces| =
      modeRate k m ^ L * (|a_nonCES| / |a_ces|) := by
  rw [ces_mode_preserved]
  simp only [modeAfterL, abs_mul]
  rw [abs_of_nonneg (pow_nonneg (modeRate_pos (by omega : 1 ≤ k) m).le L)]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:47

Module Section

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

In the same file