Documentation

Lean 4 Proof

theorem convergence_rate_cubic {k : ℕ} (hk : 2 ≤ k) (L : ℕ) (a₀ : ℝ) :
    |modeAfterL k 3 L a₀| ≤ |a₀| := by
  simp only [modeAfterL, abs_mul]
  have ⟨hpos, hlt⟩ := modeRate_in_unit_interval hk (le_refl 3)
  have hle : modeRate k 3 ^ L ≤ 1 := pow_le_one₀ hpos.le hlt.le
  calc |modeRate k 3 ^ L| * |a₀|
      = modeRate k 3 ^ L * |a₀| := by
        rw [abs_of_nonneg (pow_nonneg hpos.le L)]
    _ ≤ 1 * |a₀| :=
        mul_le_mul_of_nonneg_right hle (abs_nonneg a₀)
    _ = |a₀| := one_mul _

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:162

Module Section

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

In the same file