theorem
proved
costCompose_left_cancel
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 496.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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. -/
521structure RecognitionCostSystem (n : ℕ) where
522 cost : ℝ → ℝ
523 rcl : SatisfiesRCL cost
524 sigma : (Fin n → ℝ) → ℝ
525 W : ℕ
526 W_pos : 0 < W