`BookProof.LocalOperators.localIntegral_translation_invariant` (l : LocalField d E) (y : Fin d → ℝ) : (∫ x, l (x + y)) = ∫ x, l x

Proved

BookProof.LocalOperators.localIntegral_translation_invariant

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterLocalOperators.

BookProof.LocalOperators.localIntegral_translation_invariant (l : LocalField d E) (y : Fin d → ℝ) : (∫ x, l (x + y)) = ∫ x, l x

Formalization note: Lean 4 identifier BookProof.LocalOperators.localIntegral_translation_invariant.

Preamble

-- Generated from ChapterLocalOperators.lean — theorem BookProof.LocalOperators.localIntegral_translation_invariant
import Mathlib
import Definitions.Def_ChapterLocalOperators
open BookProof.LocalOperators



open MeasureTheory

variable {d : ℕ} {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Formal statement

theorem BookProof.LocalOperators.localIntegral_translation_invariant (l : LocalField d E) (y : Fin d → ℝ) :
    (∫ x, l (x + y)) = ∫ x, l x := by sorry

View graph