theorem
proved
tactic proof
contraction_converges
show as:
view Lean formalization →
formal statement (Lean)
35theorem contraction_converges (c : Contraction) (x₀ : ℝ) (hx : 0 < x₀) (n : ℕ)
36 (hn : 0 < n) :
37 c.contraction_rate ^ n * |x₀ - 1| < |x₀ - 1| ∨ x₀ = 1 := by
proof body
Tactic-mode proof.
38 by_cases h : x₀ = 1
39 · right; exact h
40 · left
41 have hne : |x₀ - 1| > 0 := abs_pos.mpr (sub_ne_zero.mpr h)
42 have : c.contraction_rate ^ n < 1 := by
43 calc c.contraction_rate ^ n
44 ≤ c.contraction_rate ^ 1 := by
45 apply pow_le_pow_of_le_one (le_of_lt c.rate_pos) (le_of_lt c.rate_lt_one)
46 exact hn
47 _ = c.contraction_rate := pow_one _
48 _ < 1 := c.rate_lt_one
49 exact mul_lt_of_lt_one_left hne this
50
51/-- The global J-cost minimum is unique: x = 1 (defect = 0). -/