structure
definition
PathIntegralDeepCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.PathIntegralDeep on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
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