 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
 540  W_pos := hW
 541
 542/-- The canonical recognition cost system uses the positive reals as state space. -/
 543theorem canonicalRecognitionCostSystem_domain :
 544    PositiveDomain = Set.Ioi 0 := rfl
 545
 546/-- The canonical recognition cost system inherits balance. -/
 547theorem canonicalRecognitionCostSystem_cost_one {n W : ℕ} (hW : 0 < W) :

papers checked against this theorem

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