`scaleInvarianceCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.ScaleInvarianceSelectionCert
domain: Cosmology
line: 69 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.ScaleInvarianceSelectionCert on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.