CountedOnceComposition

formal source

  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
  68  rcases hCount with ⟨P, ⟨a, b, c, d, hP⟩, hSym, hCons⟩
  69  rcases rcl_direct_theorem C hOp P a b c d hP hSym hCons with
  70    ⟨c0, hRCL⟩
  71  exact ⟨P, c0, hCons, hRCL⟩