structure
definition
ExistenceUniquenessCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ExistenceUniquenessFromCost on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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⁻¹
64 isolated : ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
65
66/-- Existence uniqueness certificate. -/
67def existenceUniquenessCert : ExistenceUniquenessCert where
68 zero_iff_one := @cost_zero_set_singleton
69 unique_member := @cost_zero_set_has_one_member
70 log_symmetric := @jcost_log_symmetric
71 isolated := @jcost_isolated_from_zero
72
73end
74end ExistenceUniquenessFromCost
75end Foundation
76end IndisputableMonolith