shiftedCompose_val

formal source

 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
 263  unfold H
 264  have hJ : 0 ≤ J x := J_nonneg x hx
 265  linarith
 266
 267/-- A positive input determines a canonical shifted-monoid element. -/
 268noncomputable def shiftedOfH (x : ℝ) (hx : 0 < x) : ShiftedCarrier :=