Chapter HermiteLadderShift

Definition

ChapterHermiteLadderShift

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

definitionsformalizationtimepiece

Formal definitions for the timepiece Lean 4 formalization (source chapter BookProof/ChapterHermiteLadderShift.lean): generated def bundle for ChapterHermiteLadderShift. See BookProof/ChapterHermiteLadderShift.lean for full context.

Definition code

import Definitions.Def_ChapterHermiteRelativeBound
import Definitions.Def_ChapterQgHermiteOscillatorEsa
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterHermiteProductBasis
import Definitions.Def_ChapterHermiteProductCore
import Definitions.Def_ChapterHyperbolicQuadraticEsa
import Definitions.Def_ChapterNavierStokesDifferentialL2
import Mathlib

namespace BookProof.HermiteLadder

end BookProof.HermiteLadder

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterHermiteLadderShift.lean

View graph