`BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent` (θ : ℝ → ℝ → ℝ) (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) : (∀ t x, dt θ t x = 0) ↔ TimeIndependent θ

Proved

BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeWeylResidual.

BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent (θ : ℝ → ℝ → ℝ) (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) : (∀ t x, dt θ t x = 0) ↔ TimeIndependent θ

Formalization note: Lean 4 identifier BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent.

Preamble

-- Generated from ChapterGaugeWeylResidual.lean — theorem BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent
import Mathlib
import Definitions.Def_ChapterGaugeWeylResidual
open BookProof.ChapterGaugeWeylResidual

Formal statement

theorem BookProof.ChapterGaugeWeylResidual.weyl_residual_iff_time_independent (θ : ℝ → ℝ → ℝ)
    (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) :
    (∀ t x, dt θ t x = 0) ↔ TimeIndependent θ := by sorry

View graph