def
definition
shiftedCompose
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 225.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
222abbrev ShiftedCarrier := {A : ℝ // (1 / 2 : ℝ) ≤ A}
223
224/-- The shifted operation `A • B = 2AB` on `[1/2, ∞)`. -/
225def shiftedCompose (A B : ShiftedCarrier) : ShiftedCarrier := by
226 refine ⟨2 * A.1 * B.1, ?_⟩
227 nlinarith [A.2, B.2]
228
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