shiftedComposeH_val

formal source

 280
 281instance : Mul ShiftedHValue := ⟨shiftedComposeH⟩
 282
 283@[simp] theorem shiftedComposeH_val (A B : ShiftedHValue) :
 284    ((A * B : ShiftedHValue) : ℝ) = 2 * A.1 * B.1 := rfl
 285
 286instance : CommSemigroup ShiftedHValue where
 287  mul := (· * ·)
 288  mul_assoc A B C := by
 289    apply Subtype.ext
 290    change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
 291    ring
 292  mul_comm A B := by
 293    apply Subtype.ext
 294    change 2 * A.1 * B.1 = 2 * B.1 * A.1
 295    ring
 296
 297/-- The `H`-value of a positive real belongs to the closed range `[1, ∞)`. -/
 298noncomputable def shiftedHValueOf (x : ℝ) (hx : 0 < x) : ShiftedHValue :=
 299  ⟨H x, H_ge_one x hx⟩
 300
 301/-! ## §5. The Defect Pseudometric -/
 302
 303/-- **Defect distance**: d(x,y) = J(x/y) measures the "cost of deviation"
 304    between two positive reals.
 305
 306    Properties:
 307    - d(x,x) = 0 (identity)
 308    - d(x,y) = d(y,x) (symmetry, from J reciprocity)
 309    - d(x,y) ≥ 0 (non-negativity) -/
 310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)
 311
 312/-- **PROVED: Defect distance is zero at identity.** -/
 313theorem defectDist_self (x : ℝ) (hx : 0 < x) : defectDist x x = 0 := by