recognition / URCAdapters / URCAdapters.ELProp / EL_prop

def

`EL_prop`

definition

show as: view math explainer →

module: IndisputableMonolith.URCAdapters.ELProp
domain: URCAdapters
line: 12 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.URCAdapters.ELProp on GitHub at line 12.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

used by

formal source

   9
  10noncomputable section
  11
  12def EL_prop : Prop :=
  13  (deriv Cost.Jlog 0 = 0) ∧ (∀ t : ℝ, Cost.Jlog 0 ≤ Cost.Jlog t)
  14
  15lemma EL_holds : EL_prop := by
  16  exact ⟨Cost.EL_stationary_at_zero, Cost.EL_global_min⟩
  17
  18end
  19
  20end URCAdapters
  21end IndisputableMonolith

papers checked against this theorem

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