At the end of Step 2 on an open the transform has order < s

Step 2.2 of the proof of Theorem 103 ends by observing that the cosupport of the controlled transform of (I, m) misses the transform of H while, H being a hypersurface of maximal contact, it lies in that transform, so that it is empty ([Kol07, 104, Step 2.2]), which is the conclusion (1) of [Kol07, Theorem 103]. This module proves it for the value of Step 2 on a relatively compact open (Step22Fam.lean).

• BlowUpSequence.forall_ord_weakTransformSeq_last_pullback_lt, BlowUpSequence.forall_ord_weakTransformSeq_last_eraseEmpty_lt — "the final weak transform has order < m everywhere" is carried along a pull-back and along the deletion of empty blow-ups, the order being read at the lift of the point.
• BO.step22FamOn_ord_lt — the value of Step 2.2 on its reading open has this property for the triple of Step 2.2 restricted to the open: for the tuned data, the cosupport of the controlled transform lies in the transform of H_r (maximal contact for the tuned ideal sheaf, by maximalContact_persistsFam restricted to the open and iteratedDeriv_tuning, carried along by [Kol07, Theorem 80 (1)]) and misses it (Lemma 102 (1) at the appended member H_r); then ord_lt_of_tuned carries the drop back through the tuning.
• step2SeqFamOn_ord_lt — for the value of Step 2 on U: the chain of Step 2.1 restricted to the next open is of order exactly s, so its final weak transform is the controlled one, which is the ideal sheaf of the triple of Step 2.2 pulled back along the lift of the restriction; the drop along the appended value of Step 2.2 carries through the concatenation, the restriction to U and the deletion of empty blow-ups.

This is the clause ord_lt of the family structure BOanFam for the local functor (LocalFunctorFam.lean).

theorem AnalyticManifold.BlowUpSequence.forall_ord_weakTransformSeq_last_pullback_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (m : ℕ) (hL : ∀ (y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length)) y < ↑m) (z : ↑↧((L.pullback h hh).toSuccession.stage (Fin.last (L.pullback h hh).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).toSuccession.length)) z < ↑m

Order < m everywhere of the final weak transform pulls back along a local analytic isomorphism ([Kol07, 34.1]): the order of the pulled-back final weak transform at a point is the order at its lift (weakTransformSeq_pullback, ord_pullback_of_isLocalDiffeomorphAt).

theorem AnalyticManifold.BlowUpSequence.forall_ord_weakTransformSeq_last_eraseEmpty_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (J : M.IdealSheaf) (m : ℕ) (hL : ∀ (y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length)) y < ↑m) (z : ↑↧(L.eraseEmpty.toSuccession.stage (Fin.last L.eraseEmpty.toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (L.eraseEmpty.toSuccession.weakTransformSeq J (Fin.last L.eraseEmpty.toSuccession.length)) z < ↑m

Order < m everywhere of the final weak transform survives the deletion of empty blow-ups ([Kol07, 32]): the last stages are identified by eraseEmptyLast.

theorem Hironaka.Manifold.BO.step22FamOn_ord_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : (s : ℕ) → BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (w : ((step22FamOn bd T s hT U hU hH hle).toSuccession.stage (Fin.last (step22FamOn bd T s hT U hU hH hle).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((step22FamOn bd T s hT U hU hH hle).toSuccession.weakTransformSeq ((step22TripleFam bd T s hT U hU hH hle).pullback (((step2FamChain bd T s hT U hU).L.stage (Fin.last (step2FamChain bd T s hT U hU).L.length)).inclusion (step2ReadOpen bd T s hT U hU)) ⋯).I (Fin.last (step22FamOn bd T s hT U hU hH hle).toSuccession.length)) w < ↑s

At the end of the value of Step 2.2 on its reading open, the weak transform of the ideal sheaf of the triple of Step 2.2 restricted to the open has order < s everywhere (the conclusion of [Kol07, 104, Step 2.2], per open). For the tuned data, the cosupport of the controlled transform lies in the transform of H_r (maximal contact for the tuned ideal sheaf by maximalContact_persistsFam restricted to the open and iteratedDeriv_tuning, carried along the sequence by [Kol07, Theorem 80 (1)]) and misses it (Lemma 102 (1) for the appended member, the greatest member being H_r); then ord_lt_of_tuned carries the drop back through the tuning.

theorem Hironaka.Manifold.step2SeqFamOn_ord_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : (s : ℕ) → BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (x : ((BO.step2SeqFamOn bd T s hT U hU hH hle).toSuccession.stage (Fin.last (BO.step2SeqFamOn bd T s hT U hU hH hle).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((BO.step2SeqFamOn bd T s hT U hU hH hle).toSuccession.weakTransformSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (BO.step2SeqFamOn bd T s hT U hU hH hle).toSuccession.length)) x < ↑s

At the end of the value of Step 2 on the open U, the weak transform of 𝓘|_U has order < s everywhere ([Kol07, Theorem 103 (1)] per open, by [Kol07, 104, Step 2.2]): the chain of Step 2.1 restricted to the next open is of order exactly s, so its final weak transform is the controlled one (isOfOrderOf), which is the ideal sheaf of the triple of Step 2.2 pulled back along the lift of the restriction (markedTransformSeq_last_pullbackLiftLast, pullback_comp); the drop along the appended value of Step 2.2 (step22FamOn_ord_lt, pulled back along the corestricted lift) carries through the concatenation (forall_ord_lt_concat_of_forall), the restriction to U and the deletion of empty blow-ups.