structure
definition
ScaleInvarianceCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.ScaleInvarianceSelectionCert on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
57theorem log_space_symmetry {x : ℝ} (hx : 0 < x) :
58 Jcost x = Jcost x⁻¹ := Jcost_symm hx
59
60structure ScaleInvarianceCert where
61 rcl : ∀ {x y : ℝ}, 0 < x → 0 < y →
62 Jcost (x * y) + Jcost (x / y) = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y
63 scale_cost_bound : ∀ {c x : ℝ}, 0 < c → 0 < x →
64 Jcost (c * x) ≤ 2 * Jcost c * Jcost x + 2 * Jcost c + 2 * Jcost x
65 free_at_unit : ∀ {x : ℝ}, 0 < x → Jcost (1 * x) = Jcost x
66 log_symmetric : ∀ {x : ℝ}, 0 < x → Jcost x = Jcost x⁻¹
67
68/-- Scale-invariance selection certificate. -/
69def scaleInvarianceCert : ScaleInvarianceCert where
70 rcl := rcl_equality
71 scale_cost_bound := scale_change_cost
72 free_at_unit := @no_scale_change_is_free
73 log_symmetric := Jcost_symm
74
75end
76end ScaleInvarianceSelectionCert
77end Cosmology
78end IndisputableMonolith