reciprocal_involution

formal source

 688noncomputable def reciprocalAuto : ℝ → ℝ := fun x => x⁻¹
 689
 690/-- **PROVED: The reciprocal map is an involution.** -/
 691theorem reciprocal_involution (x : ℝ) :
 692    reciprocalAuto (reciprocalAuto x) = x := by
 693  unfold reciprocalAuto
 694  exact inv_inv x
 695
 696/-- **PROVED: The reciprocal map preserves J-cost.** -/
 697theorem reciprocal_preserves_cost (x : ℝ) (hx : 0 < x) :
 698    J (reciprocalAuto x) = J x := by
 699  unfold reciprocalAuto
 700  exact (J_reciprocal x hx).symm
 701
 702/-- Exact level-set classification for `J` on positive reals:
 703    equal cost means equal ratio or reciprocal ratio. -/
 704theorem J_eq_iff_eq_or_inv {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 705    J y = J x ↔ y = x ∨ y = x⁻¹ := by
 706  constructor
 707  · intro h
 708    unfold J Jcost at h
 709    have hfrac : y + y⁻¹ = x + x⁻¹ := by linarith
 710    have hx0 : x ≠ 0 := ne_of_gt hx
 711    have hy0 : y ≠ 0 := ne_of_gt hy
 712    field_simp [hx0, hy0] at hfrac
 713    have hfactor : (y - x) * (x * y - 1) = 0 := by
 714      calc
 715        (y - x) * (x * y - 1) = x * y ^ 2 + x - (x ^ 2 * y + y) := by ring
 716        _ = 0 := by linarith
 717    rcases mul_eq_zero.mp hfactor with hxy | hxy
 718    · left
 719      linarith
 720    · right
 721      have hxy1 : x * y = 1 := by linarith