def
definition
shiftedHValueOf
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 298.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 :=
299 ⟨H x, H_ge_one x hx⟩
300
301/-! ## §5. The Defect Pseudometric -/
302
303/-- **Defect distance**: d(x,y) = J(x/y) measures the "cost of deviation"
304 between two positive reals.
305
306 Properties:
307 - d(x,x) = 0 (identity)
308 - d(x,y) = d(y,x) (symmetry, from J reciprocity)
309 - d(x,y) ≥ 0 (non-negativity) -/
310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)
311
312/-- **PROVED: Defect distance is zero at identity.** -/
313theorem defectDist_self (x : ℝ) (hx : 0 < x) : defectDist x x = 0 := by
314 unfold defectDist
315 rw [div_self (ne_of_gt hx)]
316 exact J_at_one
317
318/-- **PROVED: Defect distance is symmetric.** -/
319theorem defectDist_symm (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
320 defectDist x y = defectDist y x := by
321 unfold defectDist
322 have h : x / y > 0 := div_pos hx hy
323 rw [J_reciprocal (x / y) h]
324 congr 1
325 field_simp
326
327/-- **PROVED: Defect distance is non-negative.** -/
328theorem defectDist_nonneg (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :