  34  ∃ a b c d : ℝ, ∀ u v, P u v = a + b * u + c * v + d * u * v
  35
  36/-- A combiner is symmetric when exchanging its arguments does not change it. -/
  37def SymmetricCombiner (P : ℝ → ℝ → ℝ) : Prop :=
  38  ∀ u v, P u v = P v u
  39
  40/-- Counted-once composition for a comparison operator. -/
  41def CountedOnceComposition (C : ComparisonOperator) : Prop :=
  42  ∃ P : ℝ → ℝ → ℝ,
  43    CountedOnceCombiner P ∧
  44    SymmetricCombiner P ∧
  45    (∀ x y : ℝ, 0 < x → 0 < y →
  46      derivedCost C (x * y) + derivedCost C (x / y) =
  47        P (derivedCost C x) (derivedCost C y))
  48
  49/-- Counted-once composition is a special case of finite pairwise polynomial
  50closure. -/
  51theorem counted_once_to_finite_pairwise_polynomial
  52    (C : ComparisonOperator)
  53    (hCount : CountedOnceComposition C) :
  54    FinitePairwisePolynomialClosure C := by
  55  rcases hCount with ⟨P, ⟨a, b, c, d, hP⟩, hSym, hCons⟩
  56  refine ⟨P, ?_, hSym, hCons⟩
  57  refine ⟨a, b, c, d, 0, 0, ?_⟩
  58  intro u v
  59  rw [hP]
  60  ring
  61
  62/-- Counted-once operative comparison forces the RCL family. -/
  63theorem counted_once_combiner_forces_rcl
  64    (C : ComparisonOperator)
  65    (hOp : OperativePositiveRatioComparison C)
  66    (hCount : CountedOnceComposition C) :
  67    RCLFamily (derivedCost C) := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.