pith. machine review for the scientific record. sign in
theorem

off_match_positive

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.BlackBodyRadiationDeep
domain
Foundation
line
42 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.BlackBodyRadiationDeep on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  39theorem stefan_boltzmann_zero_cost : Jcost 1 = 0 := Jcost_unit0
  40
  41/-- Off matched: J-cost > 0. -/
  42theorem off_match_positive (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) : 0 < Jcost x :=
  43  Jcost_pos_of_ne_one hx hne
  44
  45structure BlackBodyRadiationDeepCert where
  46  wien_zero : Jcost 1 = 0
  47  sb_zero : Jcost 1 = 0
  48  off_match : ∀ x : ℝ, 0 < x → x ≠ 1 → 0 < Jcost x
  49
  50noncomputable def blackBodyRadiationDeepCert : BlackBodyRadiationDeepCert where
  51  wien_zero := wien_zero_cost
  52  sb_zero := stefan_boltzmann_zero_cost
  53  off_match := off_match_positive
  54
  55theorem blackBodyRadiationDeepCert_inhabited : Nonempty BlackBodyRadiationDeepCert :=
  56  ⟨blackBodyRadiationDeepCert⟩
  57
  58end
  59end BlackBodyRadiationDeep
  60end Foundation
  61end IndisputableMonolith

papers checked against this theorem (showing 1 of 1)