reciprocal_preserves_cost

formal source

 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
 722      calc
 723        y = (x⁻¹ * x) * y := by rw [inv_mul_cancel₀ hx0, one_mul]
 724        _ = x⁻¹ * (x * y) := by ring
 725        _ = x⁻¹ := by rw [hxy1, mul_one]
 726  · intro h
 727    rcases h with rfl | h