Maximal contact persists along a sequence of order ≥ s

Step 2 of the proof of [Kol07, Theorem 103] notes that under a smooth blow-up of order m the birational transform of a smooth hypersurface of maximal contact "is again a smooth hypersurface of maximal contact", and its Warning ([Kol07, 104]) insists on using these transforms rather than new hypersurfaces. maximalContact_persistsFam states this for a triple of the class BOClass s and an arbitrary sequence of order ≥ s for it, the form in which the chain of Step 2.1 supplies its sequence: the transform H_r of a hypersurface of maximal contact H is a hypersurface of maximal contact for the controlled transform I_r, that is, the ideal sheaf of H_r lies in D^{s-1} I_r. The sequence is of order exactly s (isOfOrderOf), so the ideal sheaf of H_r lies in the controlled transform of (D^{s-1} 𝓘, 1) ([Kol07, Theorem 80 (1)]), which lies in D^{s-1} of the controlled transform of (𝓘, s) ([Kol07, Corollary 77]).

The statement enters the order clause of Step 2.2 on an open (Step22FamOrdLt.lean).

theorem Hironaka.Manifold.maximalContact_persistsFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) : ⋯.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv (BO.step22TripleOf T L hge ⋯).I (s - 1)

Maximal contact persists along any sequence of order ≥ s for a triple of the class BOClass s (Step 2 of the proof of [Kol07, Theorem 103]; [Kol07, Theorem 80 (1)]): the transform H_r of a hypersurface of maximal contact H is a hypersurface of maximal contact for the controlled transform I_r. The sequence is of order exactly s (isOfOrderOf), the ideal sheaf of H_r lies in the controlled transform of (D^{s-1} 𝓘, 1) (idealSheaf_strictTransformSeq_le_markedTransformSeq), and that lies in D^{s-1} I_r (markedTransformSeq_iteratedDeriv_le, [Kol07, Corollary 77]).