theorem
proved
shiftedUnit_val
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 236.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
263 unfold H
264 have hJ : 0 ≤ J x := J_nonneg x hx
265 linarith
266