costCompose_right_cancel

formal source

 506  linarith
 507
 508/-- Right-cancellation follows from commutativity of `★`. -/
 509theorem costCompose_right_cancel {a₁ a₂ b : ℝ} (hb : 0 ≤ b)
 510    (h : a₁ ★ b = a₂ ★ b) : a₁ = a₂ := by
 511  rw [costCompose_comm a₁ b, costCompose_comm a₂ b] at h
 512  exact costCompose_left_cancel hb h
 513
 514/-! ## §5b. Recognition Cost Systems and Window Aggregation -/
 515
 516/-- The ambient domain of recognition cost systems: positive reals. -/
 517def PositiveDomain : Set ℝ := Set.Ioi 0
 518
 519/-- A recognition cost system packages a ratio cost, a conservation
 520    functional, and a finite window length. -/
 521structure RecognitionCostSystem (n : ℕ) where
 522  cost : ℝ → ℝ
 523  rcl : SatisfiesRCL cost
 524  sigma : (Fin n → ℝ) → ℝ
 525  W : ℕ
 526  W_pos : 0 < W
 527
 528/-- The canonical conservation functional from Definition 2.7:
 529    sum of logarithms on positive coordinates. -/
 530noncomputable def canonicalSigma {n : ℕ} (x : Fin n → ℝ) : ℝ :=
 531  ∑ i, Real.log (x i)
 532
 533/-- The canonical recognition cost system `(ℝ₊, J, σ, W)`. -/
 534noncomputable def canonicalRecognitionCostSystem (n W : ℕ) (hW : 0 < W) :
 535    RecognitionCostSystem n where
 536  cost := J
 537  rcl := RCL_holds
 538  sigma := canonicalSigma
 539  W := W