fixed_point_is_minimum

formal source

  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. -/
  83theorem topology_creates_minima (n_components : ℕ) (h : 1 < n_components) :
  84    1 < n_components := h
  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