IndisputableMonolith.RRF.Theorems.MonotoneArgmin

   1import Mathlib.Order.Basic
   2import Mathlib.Order.Monotone.Basic
   3import Mathlib.Data.Real.Basic
   4import Mathlib.Tactic
   5
   6/-!
   7# RRF Theorems: Monotone Transform Invariance
   8
   9If `g : ℝ → ℝ` is strictly monotone, then `argmin (g ∘ J) = argmin J`.
  10
  11This is fundamental to RRF: the "meaning" of strain is preserved under any
  12monotone rescaling. What matters is the ordering, not the absolute values.
  13
  14## Main Results
  15
  16- `argmin_comp_strictMono`: argmin is invariant under strictly monotone transforms
  17- `order_preserving_strictMono`: strict monotonicity preserves all ordering relations
  18-/
  19
  20
  21namespace IndisputableMonolith
  22namespace RRF.Theorems
  23
  24variable {State : Type*} {J : State → ℝ} {g : ℝ → ℝ}
  25
  26/-- A state x is an argmin of J if J(x) ≤ J(y) for all y. -/
  27def isArgmin (J : State → ℝ) (x : State) : Prop :=
  28  ∀ y : State, J x ≤ J y
  29
  30/-- Strictly monotone transforms preserve argmin.
  31
  32If g is strictly monotone and x is an argmin of J,
  33then x is also an argmin of g ∘ J.
  34-/
  35theorem argmin_comp_strictMono
  36    (hg : StrictMono g)
  37    (x : State) (hx : isArgmin J x) :
  38    isArgmin (g ∘ J) x := by
  39  intro y
  40  exact hg.monotone (hx y)
  41
  42/-- Strictly monotone transforms preserve the converse: if x is argmin of g ∘ J, then x is argmin of J (assuming g is onto the relevant range). -/
  43theorem argmin_of_comp_strictMono
  44    (hg : StrictMono g)
  45    (x : State) (hgx : isArgmin (g ∘ J) x) :
  46    isArgmin J x := by
  47  intro y
  48  -- g(J(x)) ≤ g(J(y)) and g strictly mono → J(x) ≤ J(y)
  49  by_contra h
  50  push_neg at h
  51  have : g (J x) > g (J y) := hg h
  52  have : ¬ (g ∘ J) x ≤ (g ∘ J) y := not_le_of_gt this
  53  exact this (hgx y)
  54
  55/-- Strictly monotone transforms preserve strict ordering. -/
  56theorem strictOrder_comp_strictMono
  57    (hg : StrictMono g)
  58    {x y : State} (hxy : J x < J y) :
  59    (g ∘ J) x < (g ∘ J) y :=
  60  hg hxy
  61
  62/-- Monotone transforms preserve weak ordering. -/
  63theorem weakOrder_comp_mono
  64    (hg : Monotone g)
  65    {x y : State} (hxy : J x ≤ J y) :
  66    (g ∘ J) x ≤ (g ∘ J) y :=
  67  hg hxy
  68
  69/-- The key theorem: strictly monotone transforms induce an equivalence on argmin sets. -/
  70theorem argmin_equiv_strictMono (hg : StrictMono g) (x : State) :
  71    isArgmin J x ↔ isArgmin (g ∘ J) x :=
  72  ⟨argmin_comp_strictMono hg x, argmin_of_comp_strictMono hg x⟩
  73
  74/-- Application: shifting J by a constant preserves argmin. -/
  75theorem argmin_add_const (c : ℝ) (x : State) :
  76    isArgmin J x ↔ isArgmin (fun s => J s + c) x := by
  77  constructor
  78  · intro h y
  79    have := h y
  80    linarith
  81  · intro h y
  82    have := h y
  83    linarith
  84
  85/-- Application: scaling J by a positive constant preserves argmin. -/
  86theorem argmin_mul_pos (c : ℝ) (hc : 0 < c) (x : State) :
  87    isArgmin J x ↔ isArgmin (fun s => c * J s) x := by
  88  have hg : StrictMono (fun t => c * t) := strictMono_mul_left_of_pos hc
  89  exact argmin_equiv_strictMono hg x
  90
  91end RRF.Theorems
  92end IndisputableMonolith
  93