midpointMap

formal source

  37noncomputable section
  38
  39/-- The midpoint map `x ↦ (x + 1)/2` is a linear contraction toward 1. -/
  40def midpointMap (x : ℝ) : ℝ := (x + 1) / 2
  41
  42/-- The midpoint map has fixed point 1. -/
  43theorem midpointMap_fixed_point : midpointMap 1 = 1 := by
  44  unfold midpointMap; norm_num
  45
  46/-- J decreases under the midpoint map for any x > 0, x ≠ 1. -/
  47theorem midpointMap_decreases_jcost {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  48    Jcost (midpointMap x) < Jcost x := by
  49  unfold midpointMap
  50  have hm_pos : 0 < (x + 1) / 2 := by positivity
  51  have hJx_eq : Jcost x = (x - 1) ^ 2 / (2 * x) := Jcost_eq_sq hx.ne'
  52  have hJm_eq : Jcost ((x + 1) / 2) = (x - 1) ^ 2 / (4 * (x + 1)) := by
  53    rw [Jcost_eq_sq hm_pos.ne']
  54    have hx1_pos : 0 < x + 1 := by linarith
  55    field_simp
  56    ring
  57  rw [hJx_eq, hJm_eq]
  58  rw [div_lt_div_iff₀ (by positivity) (by positivity)]
  59  have hne' : x - 1 ≠ 0 := sub_ne_zero.mpr hne
  60  have h_sq_pos : 0 < (x - 1) ^ 2 := by positivity
  61  nlinarith
  62
  63/-- The unique fixed point of any J-cost-decreasing map with J as Lyapunov
  64    function is x = 1. -/
  65theorem jcost_lyapunov_unique_fixed_point {f : ℝ → ℝ}
  66    (hfixed : f 1 = 1)
  67    (hdecreasing : ∀ x : ℝ, 0 < x → x ≠ 1 → Jcost (f x) < Jcost x) :
  68    ∀ y : ℝ, 0 < y → f y = y → y = 1 := by
  69  intro y hy hfy
  70  by_contra hne