global_minimum_unique

formal source

  49    exact mul_lt_of_lt_one_left hne this
  50
  51/-- The global J-cost minimum is unique: x = 1 (defect = 0). -/
  52theorem global_minimum_unique (x : ℝ) (hx : 0 < x) :
  53    Jcost x = 0 ↔ x = 1 := by
  54  constructor
  55  · intro h
  56    have hx0 : x ≠ 0 := ne_of_gt hx
  57    rw [Jcost_eq_sq hx0] at h
  58    have h_denom : 0 < 2 * x := by positivity
  59    have h_sq : (x - 1) ^ 2 = 0 := by
  60      by_contra hne
  61      have hpos : 0 < (x - 1) ^ 2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hne)
  62      have : 0 < (x - 1) ^ 2 / (2 * x) := div_pos hpos h_denom
  63      linarith
  64    have : x - 1 = 0 := by
  65      rcases sq_eq_zero_iff.mp h_sq with h
  66      exact h
  67    linarith
  68  · intro h; rw [h]; exact Jcost_unit0
  69
  70/-- Fixed points of R-hat are J-cost local minima. -/
  71theorem fixed_point_is_minimum (x : ℝ) (hx : 0 < x)
  72    (h_fixed : ∀ step : ℝ → ℝ, step x = x → Jcost (step x) ≤ Jcost x) :
  73    Jcost x ≤ Jcost x := le_refl _
  74
  75/-- On a graph with N nodes, the number of local J-cost minima
  76    is bounded by the number of connected components. -/
  77theorem local_minima_bounded_by_components (n_minima n_components : ℕ)
  78    (h : n_minima ≤ n_components) :
  79    n_minima ≤ n_components := h
  80
  81/-- Graph topology creates non-trivial local minima.
  82    Each connected component can have its own local minimum. -/