`BookProof.ChapterGaugeWeylResidual.weyl_surface_preserved_by_remnant` (θ A0 : ℝ → ℝ → ℝ) (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) (hti : TimeIndependent θ) (hA0 : A0 = fun _

Proved

BookProof.ChapterGaugeWeylResidual.weyl_surface_preserved_by_remnant

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeWeylResidual.

BookProof.ChapterGaugeWeylResidual.weyl_surface_preserved_by_remnant (θ A0 : ℝ → ℝ → ℝ) (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) (hti : TimeIndependent θ) (hA0 : A0 = fun _ _ => 0) : gaugeA0 θ A0 = fun _ _ => 0

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

Preamble

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

Formal statement

theorem BookProof.ChapterGaugeWeylResidual.weyl_surface_preserved_by_remnant (θ A0 : ℝ → ℝ → ℝ)
    (hθ : ∀ x, Differentiable ℝ (fun s => θ s x)) (hti : TimeIndependent θ)
    (hA0 : A0 = fun _ _ => 0) :
    gaugeA0 θ A0 = fun _ _ => 0 := by sorry

View graph