def definition def or abbrev

`christoffelStub`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 144noncomputable def christoffelStub : ChristoffelExpansionFacts where
 145  christoffel_expansion_minkowski := by

proof body

Definition body.

 146    intro hWF x ρ μ ν
 147    have : |(0 : ℝ)| ≤ 40 * hWF.eps ^ 2 := by
 148      have hnonneg : 0 ≤ 40 * hWF.eps ^ 2 := by
 149        have := sq_nonneg hWF.eps
 150        nlinarith
 151      simpa using hnonneg
 152    simpa using this
 153  newtonian_00_formula := by
 154    intro ng x
 155    simp [ChristoffelExpansionFacts]
 156
 157instance : ChristoffelExpansionFacts := christoffelStub
 158