655structure CostMorphism (C₁ C₂ : CostAlgebraData) where 656 /-- The underlying map on ℝ₊ -/ 657 map : ℝ → ℝ 658 /-- Preserves positivity -/ 659 pos : ∀ x, 0 < x → 0 < map x 660 /-- Multiplicative: f(xy) = f(x)·f(y) -/ 661 multiplicative : ∀ x y, 0 < x → 0 < y → map (x * y) = map x * map y 662 /-- Preserves cost: C₂.cost(f(x)) = C₁.cost(x) -/ 663 preserves_cost : ∀ x, 0 < x → C₂.cost (map x) = C₁.cost x 664 665/-- **THEOREM: The identity is a cost morphism.** -/ 666def CostMorphism.id (C : CostAlgebraData) : CostMorphism C C where 667 map := fun x => x
proof body
Definition body.
668 pos := fun _ h => h 669 multiplicative := fun _ _ _ _ => rfl 670 preserves_cost := fun _ _ => rfl 671 672/-- **THEOREM: Cost morphisms compose.** -/ 673def CostMorphism.comp {C₁ C₂ C₃ : CostAlgebraData} 674 (g : CostMorphism C₂ C₃) (f : CostMorphism C₁ C₂) : CostMorphism C₁ C₃ where 675 map := g.map ∘ f.map 676 pos := fun x hx => g.pos _ (f.pos x hx) 677 multiplicative := fun x y hx hy => by 678 simp [Function.comp] 679 rw [f.multiplicative x y hx hy, g.multiplicative _ _ (f.pos x hx) (f.pos y hy)] 680 preserves_cost := fun x hx => by 681 simp [Function.comp] 682 rw [g.preserves_cost _ (f.pos x hx), f.preserves_cost x hx] 683 684/-! ## §8. The Automorphism Group -/ 685 686/-- The **reciprocal automorphism**: x ↦ 1/x. 687 This is the fundamental symmetry of the cost algebra. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.