`BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline` : (∀ v w : LinfZ, velocityOp v * velocityOp w = velocityOp w * velocityOp v) ∧ (∀ (v : LinfZ) (j : ℤ)

Proved

BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeShiftExample.

BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline : (∀ v w : LinfZ, velocityOp v * velocityOp w = velocityOp w * velocityOp v) ∧ (∀ (v : LinfZ) (j : ℤ), velocityOp v (basisVecL2 j) = ((v : ℤ → ℝ) j : ℂ) • basisVecL2 j) ∧ (∀ m : ℤ, m ≠ 0 → ∀ v : LinfZ, shiftOp m ≠ velocityOp v) ∧ (∀ m j : ℤ, shiftOp m (basisVecL2 j) = basisVecL2 (j - m) ∧ basisVecL2 (j - m) ≠ 0)

Formalization note: Lean 4 identifier BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline.

Preamble

-- Generated from ChapterGaugeShiftExample.lean — theorem BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline
import Mathlib
import Definitions.Def_ChapterGaugeShiftExample
import Definitions.Def_ChapterContinuityUnitary
import Definitions.Def_ChapterContinuityUnitaryInfinite
import Definitions.Def_ChapterNavierStokesFullEsa
open BookProof.ChapterContinuityUnitary
open BookProof.ChapterContinuityUnitaryInfinite
open BookProof.NavierStokesFlow.FullEsa
open BookProof.NavierStokesFlow.FullEsa.NSFullData
open BookProof.ChapterGaugeShiftExample


open scoped InnerProductSpace


open BookProof.ChapterContinuityUnitaryInfinite

Formal statement

theorem BookProof.ChapterGaugeShiftExample.shift_unconstrained_gauge_fixing_headline :
    (∀ v w : LinfZ, velocityOp v * velocityOp w = velocityOp w * velocityOp v) ∧
    (∀ (v : LinfZ) (j : ℤ),
      velocityOp v (basisVecL2 j) = ((v : ℤ → ℝ) j : ℂ) • basisVecL2 j) ∧
    (∀ m : ℤ, m ≠ 0 → ∀ v : LinfZ, shiftOp m ≠ velocityOp v) ∧
    (∀ m j : ℤ, shiftOp m (basisVecL2 j) = basisVecL2 (j - m) ∧
      basisVecL2 (j - m) ≠ 0) := by sorry

View graph