 229instance : Mul ShiftedCarrier := ⟨shiftedCompose⟩
 230
 231/-- The identity element `1/2` for the shifted monoid. -/
 232noncomputable def shiftedUnit : ShiftedCarrier := ⟨1 / 2, le_rfl⟩
 233
 234noncomputable instance : One ShiftedCarrier := ⟨shiftedUnit⟩
 235
 236@[simp] theorem shiftedUnit_val : (shiftedUnit : ℝ) = 1 / 2 := rfl
 237
 238@[simp] theorem shiftedCompose_val (A B : ShiftedCarrier) :
 239    ((A * B : ShiftedCarrier) : ℝ) = 2 * A.1 * B.1 := rfl
 240
 241noncomputable instance : CommMonoid ShiftedCarrier where
 242  mul := (· * ·)
 243  mul_assoc A B C := by
 244    apply Subtype.ext
 245    change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
 246    ring
 247  one := 1
 248  one_mul A := by
 249    apply Subtype.ext
 250    change 2 * (1 / 2 : ℝ) * A.1 = A.1
 251    ring
 252  mul_one A := by
 253    apply Subtype.ext
 254    change 2 * A.1 * (1 / 2 : ℝ) = A.1
 255    ring
 256  mul_comm A B := by
 257    apply Subtype.ext
 258    change 2 * A.1 * B.1 = 2 * B.1 * A.1
 259    ring
 260
 261/-- `H(x)` lands in `[1, ∞)` on positive reals, hence in `[1/2, ∞)` as well. -/
 262theorem H_ge_one (x : ℝ) (hx : 0 < x) : 1 ≤ H x := by

papers checked against this theorem

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