The rounds on the nonmonomial part: the descent along a shrinking chain #
The rounds of order reduction on the nonmonomial part ([Kol07, 111, Step 1]; the first phase of
the modified algorithm of [Wlo09, Theorem 7.4.1], "until we drop max ord N(I) to 1") are run as
a descent through the bounds d = D, D − 1, …, t: D is a bound of ord N(𝓘) on the first
open of a shrinking chain W 0 ⊇ closure (W 1) ⊇ W 1 ⊇ ⋯ ⊇ W r of relatively compact opens
(canonically D = roundOrderOn T U₀, the maximum of ord N(𝓘) on the closure of an outer open
U₀ ⊇ W 0, see StepAFamily.lean), and at every d one link (BState.descentLink) runs on the
next two opens of the chain, r = D + 1 − t links in all (descentStateAux, descentState). At a
bound d above the current maximal order of N(𝓘) the value of the round is the empty list (the
centres of a sequence of order ≥ d lie where the order is ≥ d, and none is empty; see
BOanFam.seqOn_eq_nil), so the nonempty links are the rounds at d = max-ord N(𝓘) in the order
of the sources. The state after the last link satisfies max-ord N(𝓘_ind) ≤ t − 1 on its last
stage (descentState_bound): the exit condition of the sources at t = m, respectively t = 2.
The bound is a parameter of the descent (any D with ord N(𝓘) ≤ D on W 0, BState.initialOf):
the alignment of two descents (the compatibility of the values, their independence from the outer
open and the chain, the commutation with local isomorphisms) runs a third descent from the larger
of two bounds on the intersections of two chains, whose first links are empty.
The chain: since r depends on D, which is read on U₀, the opens are the iterated shrinkings
of the compact closure U inside U₀ (shrinkChain, from Mathlib's
exists_open_between_and_isCompact_closure): closure (W (k + 1)) ⊆ W k, every W k relatively
compact and containing closure U, closure (W 0) ⊆ U₀. The descent is stated for any such chain
and any bound; the canonical ones are chosen in StepAFamily.lean.
The initial state at a bound D: no blow-ups yet (ChainState.init), the invariant from
the pointwise bound ord N(𝓘) ≤ D on W, transported along the inclusion (NonmonomialComap,
ord_pullback_of_isLocalDiffeomorphAt). BState.initial is the case D = roundOrderOn T U₀.
Equations
- Hironaka.Manifold.BMOmod.BState.initialOf T m hcomp D hD = { toChainState := Hironaka.Manifold.ChainState.init T m W, bound := ⋯ }
Instances For
The initial state has no blow-ups.
The descent: j links from the initial state on W 0 at the bound D, giving the state on
W j at the bound D − j (for j ≤ r and j ≤ D + 1 − t: every link so far ran at a bound
d ≥ t).
Equations
- One or more equations did not get rendered due to their size.
- Hironaka.Manifold.BMOmod.descentStateAux T m hT bo hcomp hid t hm hmt W hW r hWsub D hD 0 x_3 x_4 = Hironaka.Manifold.BMOmod.BState.initialOf T m ⋯ D hD
Instances For
The number of links of the descent: D + 1 − t (zero when D < t: nothing to do).
Equations
- Hironaka.Manifold.BMOmod.descentLength t D = D + 1 - t
Instances For
The final state of the descent, after D + 1 − t links, on W (D + 1 − t)
([Kol07, 111, Step 1]; [Wlo09, Theorem 7.4.1], the modified algorithm).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The terminal bound: at the final state, max-ord N(𝓘_ind) ≤ t − 1 everywhere on the last stage
("until we drop max ord N(I) to 1" at t = 2, [Wlo09, Theorem 7.4.1]; "until its order drops
below m" at t = m, [Kol07, 111, Step 1]).