pith. machine review for the scientific record. sign in
lemma proved tactic proof

partialDeriv_v2_const

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  39lemma partialDeriv_v2_const {f : (Fin 4 → ℝ) → ℝ} {c : ℝ} (h : ∀ y, f y = c) (μ : Fin 4) (x : Fin 4 → ℝ) :
  40    partialDeriv_v2 f μ x = 0 := by

proof body

Tactic-mode proof.

  41  unfold partialDeriv_v2
  42  have h_const : (fun t => f (coordRay x μ t)) = (fun _ => c) := by
  43    funext t
  44    rw [h]
  45  rw [h_const]
  46  exact deriv_const (0 : ℝ) c
  47
  48/-- Second derivative `∂_μ∂_ν f(x)` as iterated directional derivatives. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.