`PathIntegralDeepCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PathIntegralDeep
domain: Foundation
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PathIntegralDeep on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  53theorem gaussian_approx_at_eq (hbar : ℝ) : path_weight 1 hbar = 1 := by
  54  unfold path_weight; rw [Jcost_unit0, neg_zero, zero_div, Real.exp_zero]
  55
  56structure PathIntegralDeepCert where
  57  path_weight_pos : ∀ r hbar : ℝ, 0 < path_weight r hbar
  58  path_weight_max : ∀ hbar : ℝ, 0 < hbar → ∀ r : ℝ, path_weight r hbar ≤ path_weight 1 hbar
  59  weight_one_at_eq : ∀ hbar : ℝ, path_weight 1 hbar = 1
  60
  61noncomputable def pathIntegralDeepCert : PathIntegralDeepCert where
  62  path_weight_pos := fun r hbar => path_weight_pos r hbar
  63  path_weight_max := path_weight_max_at_eq
  64  weight_one_at_eq := gaussian_approx_at_eq
  65
  66theorem pathIntegralDeepCert_inhabited : Nonempty PathIntegralDeepCert :=
  67  ⟨pathIntegralDeepCert⟩
  68
  69end
  70end PathIntegralDeep
  71end Foundation
  72end IndisputableMonolith

papers checked against this theorem

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