Getting Started

Definitions are used to introduce new concepts or objects in a precise and formal way. In Physlib we give all definitions doc-strings.

/-- For a harmonic oscillator, the Schrodinger Operator corresponding to it
is defined as the function from `ℝ → ℂ` to `ℝ → ℂ` taking

`ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ`. -/
noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
    fun x => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) x) + 1/2 * Q.m * Q.ω^2 * x^2 * ψ x

structure, inductive and abbrev also introduce new concepts in a similar way to def.

In Physlib we use lemmas for every theorem which is not a main one. For every lemma you must provide a proof.

lemma schrodingerOperator_parity (ψ : ℝ → ℂ) :
    Q.schrodingerOperator (parity ψ) = parity (Q.schrodingerOperator ψ) := by
  funext x
  have (ψ : ℝ → ℂ) : (fun x => (deriv fun x => ψ (-x)) x) = fun x => - deriv ψ (-x) := by
    funext x
    rw [← deriv_comp_neg]
  simp [schrodingerOperator, parity, this]

Theorems are significant results, but are otherwise exactly the same as lemmas.

theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
    𝓣(𝓝(ofFieldOpList φs)) =
    ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm := by
  ...

Informal definitions are definitions written in English rather than in Lean. They are given a tag (you can get a tag using lake exe make_tag), and a list of dependencies. The definition itself is written in the doc-string. They cannot be used in further results.

/-- The hubble constant defined in terms of the scale factor
as `(dₜ a) / a`.

The notation `H` is used for the `hubbleConstant`. -/
informal_definition hubbleConstant where
  deps := []
  tag := "6Z2NB"

Informal lemmas are lemmas written in English rather than in Lean. They are given a tag and a list of dependencies. The lemma and proof itself are written in the doc-string. They cannot be used in further results.

/-- The time evolution of the hubble parameter is equal to `dₜ H = - H^2 (1 + q)`. -/
informal_lemma time_evolution_hubbleConstant where
  deps := [hubbleConstant]
  tag := "6Z3BS"

Semi-formal results are like informal definitions and lemmas except the type of the definition or statement of the lemma is made formal. They are half-way between informal and formal statements. They cannot be used in further results and are also given a tag.

/-- The force on the classical harmonic oscillator is `- k x`. -/
semiformal_result "6YB2U" force_is_linear (x : ℝ → ℝ) :
  force S x = - S.k • x

Todo items are used to indicate things which are to be done. They consist of a tag and a string statement of what is to be done.

TODO "6VZHC" "Create a new folder for the damped harmonic oscillator, initially as a place-holder."