  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.