Registry · Definition IV.D164 tau-effective formalized

IV.D164 — Localized perturbations

The localized perturbation set P_n(U) is the set of admissible perturbations p in C_n^{adm} supported within a region U subset T^2 such that the superposition Omega_n^* oplus p remains admissible.

Book IV Part 5 Ch. 40

Lean Formalization

Module: TauLib.BookIV.Strong.GapMetaTheorem

Symbol: Tau.BookIV.Strong.LocalizedPerturbations