 740  ⟨x.1⁻¹, inv_pos.mpr x.2⟩
 741
 742/-- Distinguished positive constants used to close the automorphism proof. -/
 743def posOne : PosReal := ⟨1, by norm_num⟩
 744def posTwo : PosReal := ⟨2, by norm_num⟩
 745noncomputable def posHalf : PosReal := ⟨(1 / 2 : ℝ), by norm_num⟩
 746
 747@[simp] theorem posInv_inv (x : PosReal) : posInv (posInv x) = x := by
 748  apply Subtype.ext
 749  simp [posInv]
 750
 751@[simp] theorem posInv_one : posInv posOne = posOne := by
 752  apply Subtype.ext
 753  simp [posInv, posOne]
 754
 755@[simp] theorem posInv_two : posInv posTwo = posHalf := by
 756  apply Subtype.ext
 757  norm_num [posInv, posTwo, posHalf]
 758
 759@[simp] theorem posInv_half : posInv posHalf = posTwo := by
 760  apply Subtype.ext
 761  norm_num [posInv, posTwo, posHalf]
 762
 763/-- The honest automorphism type of the canonical cost algebra on `ℝ_{>0}`. -/
 764def JAut : Type :=
 765  { f : PosReal → PosReal //
 766      (∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y)) ∧
 767      (∀ x : PosReal, J (f x).1 = J x.1) }
 768
 769namespace JAut
 770
 771instance : CoeFun JAut (fun _ => PosReal → PosReal) := ⟨fun f => f.1⟩
 772
 773/-- Multiplicativity of a `J`-automorphism. -/

papers checked against this theorem

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