The rounds on the nonmonomial part: the value on a relatively compact open #
The value of the rounds on the nonmonomial part on a relatively compact open U
([Kol07, 111, Step 1]; the first phase of the modified algorithm of [Wlo09, Theorem 7.4.1]), read
per open as every family of the library is [Wlo09, Theorem 2.0.3 (1)]: the canonical exhaustion of
the manifold (exhaustion, exhaustionIdx) gives an outer open U₀ ⊇ closure U on which the bound
D = roundOrderOn T U₀ is read; the descent of StepAChain.lean runs its D + 1 − t links along
the canonical chain of iterated shrinkings of closure U inside U₀ (shrinkChain); its final
state, on an open containing closure U, is restricted to U and its empty blow-ups are deleted
[Kol07, 32]. This is stepAFamOn T m hT bo hcomp hid t hm hmt U hU: a smooth blow-up sequence of
order ≥ m for (𝓘|U, m) (stepAFamOn_isOfOrderGe) with no empty centre
(stepAFamOn_noEmptyCenters). The terminal bound max-ord N(𝓘_ind) ≤ t − 1 is read on the chain
state before the deletion (stepAChainState_bound); the later steps of both algorithms continue
from that state.
The index of the exhaustion is a choice; the independence of the value from it, up to empty
blow-ups, is stepAFamOn_eq_of_outer, and the compatibility of the values is stepAFamOn_compat.
The canonical opens #
The outer open U₀ of the canonical exhaustion, containing closure U; the bound D is read
on it.
Equations
Instances For
The bound D = roundOrderOn T U₀, the maximum of ord N(𝓘) on the closure of U₀.
Equations
Instances For
The number of links, D + 1 − t.
Equations
- Hironaka.Manifold.BMOmod.stepALinks T t U hU = Hironaka.Manifold.BMOmod.stepABound T U hU + 1 - t
Instances For
The canonical chain: the iterated shrinkings of closure U inside U₀ (shrinkChain).
Equations
- Hironaka.Manifold.BMOmod.stepAChainOpens U hU k = Hironaka.Manifold.shrinkChain (closure ↑U) (Hironaka.Manifold.BMOmod.stepAOuter U hU) hU ⋯ k
Instances For
The bound stepABound T U hU holds on the first open of the canonical chain of U: the bound
hypothesis of the descent along it.
The chain state and the value #
The final chain state over the inner open of U: the D + 1 − t links of the descent along
the canonical chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The terminal bound of the chain state: max-ord N(𝓘_ind) ≤ t − 1 on its last stage (the exit
condition of the rounds; the input of the later steps).
The value of the rounds on the nonmonomial part on U ([Kol07, 111, Step 1];
[Wlo09, Theorem 7.4.1]): the list of the final chain state restricted to U, its empty blow-ups
deleted [Kol07, 32].
Equations
- Hironaka.Manifold.BMOmod.stepAFamOn T m hT bo hcomp hid t hm hmt U hU = ((Hironaka.Manifold.BMOmod.stepAChainState T m hT bo ⋯ ⋯ t hm hmt U hU).L.pullback (M.restrictLE ⋯) ⋯).eraseEmpty
Instances For
The value has no empty blow-ups [Kol07, 32].
The value is a smooth blow-up sequence of order ≥ m starting with (𝓘|U, m, E|U): the
invariant of the chain restricted along the last inclusion, kept by the deletion of empty
blow-ups.