shiftedOfH

formal source

 265  linarith
 266
 267/-- A positive input determines a canonical shifted-monoid element. -/
 268noncomputable def shiftedOfH (x : ℝ) (hx : 0 < x) : ShiftedCarrier :=
 269  ⟨H x, by
 270    have hHx : 1 ≤ H x := H_ge_one x hx
 271    linarith⟩
 272
 273/-- The narrower `[1, ∞)` range supporting the actual values of `H`. -/
 274abbrev ShiftedHValue := {A : ℝ // 1 ≤ A}
 275
 276/-- The shifted operation is closed on the `H`-value range `[1, ∞)`. -/
 277def shiftedComposeH (A B : ShiftedHValue) : ShiftedHValue := by
 278  refine ⟨2 * A.1 * B.1, ?_⟩
 279  nlinarith [A.2, B.2]
 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 :=