The monomial phase terminates: the measure Σ_D a_D

The monomial phase at the mark 1 terminates because each step lowers Σ_D a_D, the sum of the exponents of 𝓘 along the boundary components ([Wlo09, §6, Step 2b]: "the invariant ν drops", and the remarks after [Wlo09, Theorem 2.0.3]; [Kol07, Definition–Lemma 110]). The measure of a triple S is

step2bMeasure S = Σ_{k, E^k ≠ ∅} sup_{x ∈ E^k} ord_{E^k} 𝓘 (x) (in ℕ∞),

the sum over the finitely many nonempty members (the finiteness clause of BMOClass) of the supremum along the member of the order of 𝓘 along it (the supremum over the points of a member is the maximum of the exponents of its components, the order along a member being constant on its connected components). The exponents after one step (Step2bExponent.lean) give: the supremum of the new member is one less than that of the top member (memberSup_inr_add_one_le), the suprema of the other members are unchanged (memberSup_inl_le), the strict transform of the top member has supremum 0; so step2bMeasure S' + 1 ≤ step2bMeasure S (step2bMeasure_stepTriple_add_one_le). The measure is finite when the order of 𝓘 is bounded (on a relatively compact open, bddAbove_ord_on_compact: step2bMeasure_le), and it is at least 1 while a member is active (one_le_step2bMeasure_of_nonempty). Hence the phase stabilises at the fuel step2bMeasure S (step2bPhase_succ_eq_of_step2bMeasure_le, step2bPhase_eq_of_step2bMeasure_le): the complete phase is step2bPhase k for any k ≥ step2bMeasure S.

theorem Manifold.IdealSheaf.ordAlongIdeal_congr_stalk_left {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D D' J : IdealSheaf 𝒪) {a : ↑X} (h : D.stalkIdeal a = D'.stalkIdeal a) : D.ordAlongIdeal J a = D'.ordAlongIdeal J a

The order along D depends only on the stalk of D at the point.

The measure

noncomputable def Hironaka.Manifold.BMOmod.memberSup {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (k : S.F.ι) : ℕ∞

The supremum along the member E^k of the order of 𝓘 along E^k: the maximal exponent of the components of E^k (0 for an empty member).

Equations

• Hironaka.Manifold.BMOmod.memberSup S k = ⨆ (x : ↑(S.F.hyp k)), ⋯.idealSheaf.ordAlongIdeal S.I ↑x

noncomputable def Hironaka.Manifold.BMOmod.step2bMeasure {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (hS : Manifold.AnalyticTriple.BMOClass 1 S) : ℕ∞

The measure Σ_D a_D of a triple: the sum over its nonempty members of the maximal exponent along the member ([Wlo09, §6, Step 2b]).

Equations

• Hironaka.Manifold.BMOmod.step2bMeasure S hS = ∑ k ∈ S.F.nonemptyFinset ⋯, Hironaka.Manifold.BMOmod.memberSup S k

theorem Hironaka.Manifold.BMOmod.ordAlong_le_memberSup {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) {k : S.F.ι} {x : M.carrier} (hx : x ∈ S.F.hyp k) : ⋯.idealSheaf.ordAlongIdeal S.I x ≤ memberSup S k

theorem Hironaka.Manifold.BMOmod.memberSup_le_step2bMeasure {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (hS : Manifold.AnalyticTriple.BMOClass 1 S) {k : S.F.ι} (hk : k ∈ S.F.nonemptyFinset ⋯) : memberSup S k ≤ step2bMeasure S hS

theorem Hironaka.Manifold.BMOmod.step2bMeasure_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (hS : Manifold.AnalyticTriple.BMOClass 1 S) {A : ℕ} (hA : ∀ (x : ↑↧M.carrier), Manifold.IdealSheaf.ord S.I x ≤ ↑A) : step2bMeasure S hS ≤ (S.F.nonemptyFinset ⋯).card • ↑A

On a triple whose order is bounded by A (every triple restricted to a relatively compact open, bddAbove_ord_on_compact) the measure is at most (number of nonempty members) · A; in particular it is finite.

theorem Hironaka.Manifold.BMOmod.step2bMeasure_ne_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (hS : Manifold.AnalyticTriple.BMOClass 1 S) {A : ℕ} (hA : ∀ (x : ↑↧M.carrier), Manifold.IdealSheaf.ord S.I x ≤ ↑A) : step2bMeasure S hS ≠ ⊤

theorem Hironaka.Manifold.BMOmod.one_le_step2bMeasure_of_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (hS : Manifold.AnalyticTriple.BMOClass 1 S) (hne : (activeMembers S).Nonempty) : 1 ≤ step2bMeasure S hS

While a member is active the measure is at least 1 (the active member is nonempty and carries a point of order ≥ 1 along it).

One step lowers the measure

theorem Hironaka.Manifold.BMOmod.stepTriple_isSnc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : ⋯ = ⋯

def Hironaka.Manifold.BMOmod.inlIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (k : T.F.ι) : (stepTriple T hfin hne).F.ι

The index of a strict transform in the family after the step.

Equations

• Hironaka.Manifold.BMOmod.inlIdx T hfin hne k = toLex (Sum.inl k)

def Hironaka.Manifold.BMOmod.inrIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : (stepTriple T hfin hne).F.ι

The index of the new member in the family after the step.

Equations

• Hironaka.Manifold.BMOmod.inrIdx T hfin hne = toLex (Sum.inr PUnit.unit)

theorem Hironaka.Manifold.BMOmod.inlIdx_def {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (k : T.F.ι) : inlIdx T hfin hne k = toLex (Sum.inl k)

theorem Hironaka.Manifold.BMOmod.inrIdx_def {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : inrIdx T hfin hne = toLex (Sum.inr PUnit.unit)

theorem Hironaka.Manifold.BMOmod.ordAlong_stepCenter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {y : M.carrier} (hy : y ∈ step2bCenter T hfin hne) : ⋯.idealSheaf.ordAlongIdeal T.I y = ⋯.idealSheaf.ordAlongIdeal T.I y

At a point of the centre Z the order along Z is the order along the top member E^j (they agree near the point, Z being open in E^j).

theorem Hironaka.Manifold.BMOmod.memberSup_inr_add_one_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : memberSup (stepTriple T hfin hne) (inrIdx T hfin hne) + 1 ≤ memberSup T (topMember T hfin hne)

The new member's sup is one less than the top member's: sup_{D'} + 1 ≤ sup_{E^j} (ordAlong_stepIdeal_inr_add_one at each point of D' = π⁻¹(Z)).

theorem Hironaka.Manifold.BMOmod.memberSup_inl_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (k : T.F.ι) : memberSup (stepTriple T hfin hne) (inlIdx T hfin hne k) ≤ memberSup T k

The sup of a strict transform is at most the sup of its member (ordAlong_stepIdeal_inl_of_ne for k ≠ j; for the top member the strict transform's orders are those of E^j off Z).

theorem Hironaka.Manifold.BMOmod.memberSup_inl_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : memberSup (stepTriple T hfin hne) (inlIdx T hfin hne (topMember T hfin hne)) = 0

The strict transform of the top member has sup 0: its points lie off the positive locus.

theorem Hironaka.Manifold.BMOmod.nonemptyFinset_stepTriple_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : (stepTriple T hfin hne).F.nonemptyFinset ⋯ ⊆ Finset.image (inlIdx T hfin hne) (T.F.nonemptyFinset ⋯) ∪ {inrIdx T hfin hne}

A nonempty strict transform lies over a nonempty member.

theorem Hironaka.Manifold.BMOmod.inlIdx_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Function.Injective (inlIdx T hfin hne)

theorem Hironaka.Manifold.BMOmod.step2bMeasure_stepTriple_add_one_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : step2bMeasure (stepTriple T hfin hne) ⋯ + 1 ≤ step2bMeasure T hT

One step of the monomial phase lowers the measure by at least one: step2bMeasure (stepTriple) + 1 ≤ step2bMeasure T ([Wlo09, §6, Step 2b]; [Kol07, Definition–Lemma 110]).

Stabilisation: the phase is complete at the fuel step2bMeasure

theorem Hironaka.Manifold.BMOmod.step2bPhase_succ_eq_of_step2bMeasure_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : step2bMeasure T hT ≤ ↑k → step2bPhase (k + 1) T hT = step2bPhase k T hT

Termination: once the fuel reaches the measure the phase does not grow, step2bPhase (k + 1) = step2bPhase k for step2bMeasure T ≤ k. Induction on k: at k = 0 no member is active (one_le_step2bMeasure_of_nonempty); otherwise the step lowers the measure by one (step2bMeasure_stepTriple_add_one_le).

theorem Hironaka.Manifold.BMOmod.step2bPhase_eq_of_step2bMeasure_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {k : ℕ} (hk : step2bMeasure T hT ≤ ↑k) (m : ℕ) : step2bPhase (k + m) T hT = step2bPhase k T hT

The complete phase: step2bPhase k is the same list for every fuel k ≥ step2bMeasure T.