def
definition
zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Fields.Scalar on GitHub at line 24.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
21 eval (constant c) x = c := rfl
22
23/-- Zero scalar field. -/
24def zero : ScalarField := constant 0
25
26theorem zero_eval (x : Fin 4 → ℝ) : eval zero x = 0 := rfl
27
28/-- Scalar field addition. -/
29def add (φ₁ φ₂ : ScalarField) : ScalarField :=
30 { ψ := fun x => φ₁.ψ x + φ₂.ψ x }
31
32/-- Scalar multiplication. -/
33def smul (c : ℝ) (φ : ScalarField) : ScalarField :=
34 { ψ := fun x => c * φ.ψ x }
35
36theorem add_comm (φ₁ φ₂ : ScalarField) :
37 ∀ x, eval (add φ₁ φ₂) x = eval (add φ₂ φ₁) x := by
38 intro x
39 simp [eval, add]
40 ring
41
42theorem smul_zero (φ : ScalarField) :
43 ∀ x, eval (smul 0 φ) x = 0 := by
44 intro x
45 simp [eval, smul]
46
47/-- Directional derivative of scalar field in direction μ. -/
48noncomputable def directional_deriv (φ : ScalarField) (μ : Fin 4) (x : Fin 4 → ℝ) : ℝ :=
49 let h := (0.001 : ℝ)
50 let x_plus := fun ν => if ν = μ then x ν + h else x ν
51 (φ.ψ x_plus - φ.ψ x) / h
52
53/-- Directional derivative is linear in the field. -/
54theorem deriv_add (φ₁ φ₂ : ScalarField) (μ : Fin 4) (x : Fin 4 → ℝ) :