`faster_contraction_faster_thinking`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.RHatFixedPoint
domain: Foundation
line: 88 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RHatFixedPoint on GitHub at line 88.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  85
  86/-- The convergence rate determines thinking speed:
  87    smaller contraction rate = faster convergence = faster thinking. -/
  88theorem faster_contraction_faster_thinking (c₁ c₂ : ℝ)
  89    (h₁ : 0 < c₁) (h₂ : 0 < c₂)
  90    (h_faster : c₁ < c₂) (error : ℝ) (he : 0 < error) (n : ℕ) :
  91    c₁ ^ n * error ≤ c₂ ^ n * error := by
  92  apply mul_le_mul_of_nonneg_right
  93  · exact pow_le_pow_left₀ (le_of_lt h₁) (le_of_lt h_faster) n
  94  · exact le_of_lt he
  95
  96end IndisputableMonolith.Foundation.RHatFixedPoint

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.