ratioCost

formal source

  13namespace LogicAsFunctionalEquation
  14
  15/-- The ratio-derived cost of a two-argument comparison. -/
  16@[simp] def ratioCost (C : ComparisonOperator) : ℝ → ℝ :=
  17  fun r => C r 1
  18
  19/-- Scale-invariant comparison factors through the positive ratio `x / y`. -/
  20theorem scale_free_comparison_factors_through_ratio
  21    (C : ComparisonOperator)
  22    (hScale : ScaleInvariant C) :
  23    ∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y) := by
  24  refine ⟨ratioCost C, ?_⟩
  25  intro x y hx hy
  26  unfold ratioCost
  27  have hy_inv_pos : 0 < y⁻¹ := inv_pos.mpr hy
  28  have hscale := hScale x y y⁻¹ hx hy hy_inv_pos
  29  have hleft : y⁻¹ * x = x / y := by
  30    rw [div_eq_mul_inv, mul_comm]
  31  have hright : y⁻¹ * y = 1 := by
  32    exact inv_mul_cancel₀ (ne_of_gt hy)
  33  calc
  34    C x y = C (y⁻¹ * x) (y⁻¹ * y) := hscale.symm
  35    _ = C (x / y) 1 := by rw [hleft, hright]
  36
  37/-- The ratio factor is unique on positive ratios. -/
  38theorem ratio_factor_unique
  39    (C : ComparisonOperator) (F G : ℝ → ℝ)
  40    (hF : ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y))
  41    (hG : ∀ x y : ℝ, 0 < x → 0 < y → C x y = G (x / y)) :
  42    ∀ r : ℝ, 0 < r → F r = G r := by
  43  intro r hr
  44  have hF' := hF r 1 hr one_pos
  45  have hG' := hG r 1 hr one_pos
  46  simpa using hF'.symm.trans hG'