docs: Fix typos in doc-strings

PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean

@@ -667,7 +667,7 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
   obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V
   have hUV : ⟦U⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftRelation_equiv.symm hU.1))
   by_cases ha : [V]ud ≠ 0 ∨ [V]us ≠ 0
-  · have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simplier
+  · have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simpler
       by_contra hn
       simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hn
       have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by
@@ -681,7 +681,7 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
     use (- arg ([U]ub))
     rw [← hUV]
     exact hU.1
-  · have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by -- should be much simplier
+  · have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by -- should be much simpler
       simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at ha
       have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by
         rw [hUV]

PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean

@@ -13,7 +13,7 @@ import Mathlib.Data.Fintype.Card
 
 /-- The type `CreateAnnihilate` is the type containing two elements `create` and `annihilate`.
   This type is used to specify if an operator is a creation, or annihilation, operator
-  or the sum thereof or integral thereover etc. -/
+  or the sum thereof or integral thereof etc. -/
 inductive CreateAnnihilate where
   | create : CreateAnnihilate
   | annihilate : CreateAnnihilate

PhysLean/QFT/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -50,15 +50,15 @@ remark wicks_theorem_context := "
   In perturbative quantum field theory, Wick's theorem allows
   us to expand expectation values of time-ordered products of fields in terms of normal-orders
   and time contractions.
-  The theorem is used to simplify the calculation of scattering amplitudes, and is the precurser
+  The theorem is used to simplify the calculation of scattering amplitudes, and is the precursor
   to Feynman diagrams.
 
   There are actually three different versions of Wick's theorem used.
   The static version, the time-dependent version, and the normal-ordered time-dependent version.
   PhysLean contains a formalization of all three of these theorems in complete generality for
   mixtures of bosonic and fermionic fields.
 
-  The statement of these theorems for bosons is simplier then when fermions are involved, since
+  The statement of these theorems for bosons is simpler then when fermions are involved, since
   one does not have to worry about the minus-signs picked up on exchanging fields."
 
 /--

PhysLean/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -41,7 +41,7 @@ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ
 namespace FieldOpFreeAlgebra
 
 remark naming_convention := "
-  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
+  For mathematical objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
   may be given to
   their names to indicate that they are related to the free algebra.
   This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined

PhysLean/QFT/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -223,7 +223,7 @@ open FieldStatistic
 -/
 
 /-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
-  `𝓕.normalOrderList φs` is the list `φs` normal-ordered using ther
+  `𝓕.normalOrderList φs` is the list `φs` normal-ordered using the
   insertion sort algorithm. It puts creation operators on the left and annihilation operators on
   the right. For example:
 

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean

@@ -277,7 +277,7 @@ open Finset
   for any real `c`.
   The proof of this result relies on the expansion of `e ^ (I c x)`
   in terms of `x^r/r!` and using `orthogonal_power_of_mem_orthogonal`
-  along with integrablity conditions. -/
+  along with integrability conditions. -/
 lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (c : ℝ) : ∫ x : ℝ, Complex.exp (Complex.I * c * x) *

PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean

@@ -21,12 +21,13 @@ import Mathlib.Algebra.Star.Basic
 namespace QuantumMechanics
 
 namespace OneDimension
+
 noncomputable section
 
 /-- The Hilbert space for a one dimensional quantum system is defined as
   the space of almost-everywhere equal equivalence classes of square integrable functions
   from `ℝ` to `ℂ`. -/
-noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
+abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
 
 namespace HilbertSpace
 open MeasureTheory
@@ -39,7 +40,7 @@ lemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) :
     AEStronglyMeasurable f := by
   exact h.1
 
-/-- A function `f` statisfies `MemHS f` if and only if it is almost everywhere
+/-- A function `f` satisfies `MemHS f` if and only if it is almost everywhere
   strongly measurable, and square integrable. -/
 lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
     AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by

scripts/MetaPrograms/notes.lean

@@ -148,7 +148,7 @@ def perturbationTheory : Note where
     .h1 "Introduction",
     .name `FieldSpecification.wicks_theorem_context .incomplete,
     .p "In this note we walk through the important parts of the proof of the three versions of
-      Wick's theorem for field operators containing carrying both fermionic and bosonic statitics,
+      Wick's theorem for field operators containing carrying both fermionic and bosonic statistics,
       as it appears in PhysLean. Not every lemma or definition is covered here.
       The aim is to give just enough that the story can be understood.",
     .p "
@@ -302,11 +302,11 @@ def harmonicOscillator : Note where
      Lean 4, as part of the larger project PhysLean.
      What this means is that every definition and theorem in this note has been formally checked
      for mathematical correctness for by a computer. There are a number of
-     motivations for doing this which are dicussed <a href = 'https://heplean.com'>here</a>.",
+     motivations for doing this which are discussed <a href = 'https://heplean.com'>here</a>.",
     .p "Note that we do not give every definition and theorem which is part of
       the formalization.
      Our goal is give key aspects, in such a way that we hope this note will be useful
-     to newcomers to Lean or those intrested in simply intrested in learning about the
+     to newcomers to Lean or those simply intrested in learning about the
      quantum harmonic oscillator.",
     .h1 "Hilbert Space",
     .name ``QuantumMechanics.OneDimension.HilbertSpace .complete,