theorem
proved
tactic proof
even_function_deriv_zero
show as:
view Lean formalization →
formal statement (Lean)
438theorem even_function_deriv_zero (G : ℝ → ℝ)
439 (hEven : ∀ t, G (-t) = G t)
440 (hDiff : DifferentiableAt ℝ G 0) :
441 deriv G 0 = 0 := by
proof body
Tactic-mode proof.
442 -- The functions (fun t => G(-t)) and G are equal everywhere
443 have hfun_eq : (fun t => G (-t)) = G := funext hEven
444 -- So their derivatives at 0 must be equal
445 have hderiv_eq : deriv (fun t => G (-t)) 0 = deriv G 0 := by simp only [hfun_eq]
446 -- Compute deriv (fun t => G(-t)) 0 using chain rule
447 have hchain : deriv (fun t => G (-t)) 0 = -(deriv G 0) := by
448 have hcomp : (fun t => G (-t)) = G ∘ (fun t => -t) := rfl
449 rw [hcomp]
450 rw [deriv_comp (0 : ℝ) (by simp only [neg_zero]; exact hDiff) differentiable_neg.differentiableAt]
451 simp only [neg_zero, deriv_neg', mul_neg_one]
452 -- Now: hderiv_eq says deriv (G ∘ neg) 0 = deriv G 0
453 -- hchain says deriv (G ∘ neg) 0 = -(deriv G 0)
454 rw [hchain] at hderiv_eq
455 linarith
456
457/-- **Axiom (Separable Combiner Forces Flat ODE)**: Under the structural axioms,
458 if P is separable (hence P = 2u + 2v), then G_of F satisfies G'' = 1.
459
460 Proof sketch: From G(t+u) + G(t-u) = 2G(t) + 2G(u), differentiate twice in u at u=0:
461 2G''(t) = 2G''(0) = 2, hence G''(t) = 1. -/