OperativePositiveRatioComparison

formal source

  21/-- An operative positive-ratio comparison is a continuous, nontrivial
  22comparison operator satisfying identity, symmetric single-valued comparison,
  23and scale invariance on positive arguments. -/
  24structure OperativePositiveRatioComparison (C : ComparisonOperator) : Prop where
  25  identity : Identity C
  26  non_contradiction : NonContradiction C
  27  continuous : ExcludedMiddle C
  28  scale_invariant : ScaleInvariant C
  29  non_trivial : NonTrivial C
  30
  31/-- Finite pairwise polynomial closure is the polynomial route-independence
  32condition from the Level-1 logic-as-functional-equation module. -/
  33def FinitePairwisePolynomialClosure (C : ComparisonOperator) : Prop :=
  34  RouteIndependence C
  35
  36/-- Scale invariance descends a two-argument comparison to a cost on the
  37positive ratio of the arguments. -/
  38theorem operative_descends_to_ratio
  39    (C : ComparisonOperator)
  40    (hOp : OperativePositiveRatioComparison C) :
  41    ∀ x y : ℝ, 0 < x → 0 < y → C x y = derivedCost C (x / y) := by
  42  intro x y hx hy
  43  unfold derivedCost
  44  have hy_inv_pos : 0 < y⁻¹ := inv_pos.mpr hy
  45  have hscale := hOp.scale_invariant x y y⁻¹ hx hy hy_inv_pos
  46  have hleft : y⁻¹ * x = x / y := by
  47    rw [div_eq_mul_inv, mul_comm]
  48  have hright : y⁻¹ * y = 1 := by
  49    exact inv_mul_cancel₀ (ne_of_gt hy)
  50  calc
  51    C x y = C (y⁻¹ * x) (y⁻¹ * y) := hscale.symm
  52    _ = C (x / y) 1 := by rw [hleft, hright]
  53
  54/-- Operative comparisons have reciprocal-symmetric derived costs. -/