cost_zero_set_singleton

formal source

  30noncomputable section
  31
  32/-- The cost-zero set is exactly {1}. -/
  33theorem cost_zero_set_singleton :
  34    ∀ x : ℝ, 0 < x → (Jcost x = 0 ↔ x = 1) := by
  35  intro x hx
  36  constructor
  37  · intro h
  38    by_contra hne
  39    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  40  · rintro rfl; exact Jcost_unit0
  41
  42/-- The cost-zero set in ℝ+ has cardinality 1 (in the sense that any two
  43    members are equal). -/
  44theorem cost_zero_set_has_one_member {x y : ℝ}
  45    (hx : 0 < x) (hy : 0 < y)
  46    (hJx : Jcost x = 0) (hJy : Jcost y = 0) :
  47    x = y := by
  48  rw [(cost_zero_set_singleton x hx).mp hJx,
  49      (cost_zero_set_singleton y hy).mp hJy]
  50
  51/-- J-cost is symmetric in log-ratio sense. -/
  52theorem jcost_log_symmetric {x : ℝ} (hx : 0 < x) :
  53    Jcost x = Jcost x⁻¹ := Jcost_symm hx
  54
  55/-- Away from 1, J-cost is strictly positive (isolation). -/
  56theorem jcost_isolated_from_zero {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  57    0 < Jcost x := Jcost_pos_of_ne_one x hx hne
  58
  59structure ExistenceUniquenessCert where
  60  zero_iff_one : ∀ {x : ℝ}, 0 < x → (Jcost x = 0 ↔ x = 1)
  61  unique_member : ∀ {x y : ℝ}, 0 < x → 0 < y →
  62    Jcost x = 0 → Jcost y = 0 → x = y
  63  log_symmetric : ∀ {x : ℝ}, 0 < x → Jcost x = Jcost x⁻¹