The rounds on the nonmonomial part: the compatible family #
With stepAFamOn_compat and stepAFamOn_noEmptyCenters the values of the rounds on the
nonmonomial part form the compatible family of the rounds,
stepAFam : CompatibleFamily T ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6];
[Kol07, 32]).
noncomputable def
Hironaka.Manifold.BMOmod.stepAFam
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
:
The compatible family of the rounds on the nonmonomial part: the value stepAFamOn on every
relatively compact open, no empty centres [Kol07, 32], compatible under restriction
([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]).
Equations
- One or more equations did not get rendered due to their size.