substitutivity_forces_factorization

formal source

  54because the compound cost depends only on the mismatch, not on the
  55specific ratio realizing it.  Therefore the compound cost descends
  56to a function of `(J(x), J(y))`. -/
  57def substitutivity_forces_factorization
  58    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
  59    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  60    (P : ℝ → ℝ → ℝ)
  61    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
  62      J (x * y) + J (x / y) = P (J x) (J y)) :
  63    ContextualSubstitutivity J :=
  64  ⟨P, hComp⟩
  65
  66/-- Symmetry of the combiner follows from commutativity of `(ℝ₊, ×)`:
  67`J(xy) + J(x/y) = J(yx) + J(y/x)` because `xy = yx` and
  68`J(x/y) = J(y/x)` by reciprocal symmetry. -/
  69theorem combiner_symmetric
  70    (J : ℝ → ℝ)
  71    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  72    (P : ℝ → ℝ → ℝ)
  73    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
  74      J (x * y) + J (x / y) = P (J x) (J y))
  75    (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a) :
  76    ∀ u v, P u v = P v u := by
  77  intro u v
  78  obtain ⟨x, hx, hJx⟩ := hSurj u
  79  obtain ⟨y, hy, hJy⟩ := hSurj v
  80  have h1 := hComp x y hx hy
  81  have h2 := hComp y x hy hx
  82  rw [hJx, hJy] at h1
  83  rw [hJy, hJx] at h2
  84  have hxy : x * y = y * x := mul_comm x y
  85  have hrecip : J (x / y) = J (y / x) := by
  86    rw [hSym (x / y) (div_pos hx hy)]
  87    congr 1