costCompose_sub_left

formal source

 487
 488/-- Subtracting two raw cost-compositions factors through the positive
 489    coefficient `2a + 2`. -/
 490theorem costCompose_sub_left (a b₁ b₂ : ℝ) :
 491    a ★ b₁ - a ★ b₂ = (2 * a + 2) * (b₁ - b₂) := by
 492  unfold costCompose
 493  ring
 494
 495/-- Equation (2.6): left-cancellation holds on the nonnegative cost range. -/
 496theorem costCompose_left_cancel {a b₁ b₂ : ℝ} (ha : 0 ≤ a)
 497    (h : a ★ b₁ = a ★ b₂) : b₁ = b₂ := by
 498  have hsub : a ★ b₁ - a ★ b₂ = 0 := sub_eq_zero.mpr h
 499  rw [costCompose_sub_left] at hsub
 500  have hcoeff : 2 * a + 2 ≠ 0 := by
 501    linarith
 502  have hdiff : b₁ - b₂ = 0 := by
 503    rcases mul_eq_zero.mp hsub with hzero | hzero
 504    · exact False.elim (hcoeff hzero)
 505    · exact hzero
 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. -/