The input piece family of the monomial procedure on a relatively compact open set

On an analytic manifold the monomial procedure of [Kol07, 111, Step 3] is run on a relatively compact open set U, as every step of the analytic order reduction is ([Wlo09, Theorem 2.0.3 (1)]). For a triple T = (M, 𝓘, E) the ambient pieces are the connected components of the members of E (ComponentIndex, the index set of the monomial part of BMO/MonomialPart.lean), each with its exponent componentExponent, the order of 𝓘 along it. The ambient pieces form a locally finite family, so only finitely many meet the compact set closure U: the meeting pieces. The input piece family on M.restrict U (inputFamily) has as pieces the traces D ∩ U of the meeting pieces D, enumerated; the label of a piece is the position of its member among the finitely many members having a meeting piece, in the order of the members (inputEmb); its exponent is the ambient exponent. It realises the boundary E|_U of the restricted triple (inputFamily_realizes): a restricted member is the union of the traces of its meeting components, members without a meeting piece are empty on U, and distinct components of one member are disjoint. It satisfies the invariants of the combinatorial state for (n, m) when T is in the class BMOClass m (inputFamily_isValid).

The pieces are the traces of the ambient components rather than the connected components of the restricted members: an ambient component may meet U in infinitely many connected components. The monomial part of the restricted triple, which is indexed by the components of the restricted members, is nevertheless the monomial ideal of the input family (BMO/Step3Monomial/InputMonomial.lean).

noncomputable def Hironaka.Manifold.BMO.meetingPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Finset (ComponentIndex T.F)

The finitely many ambient pieces (connected components of the boundary members) meeting closure U: the components form a locally finite family and closure U is compact.

Equations

• Hironaka.Manifold.BMO.meetingPieces T U hU = ⋯.toFinset

theorem Hironaka.Manifold.BMO.mem_meetingPieces_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {i : ComponentIndex T.F} : i ∈ meetingPieces T U hU ↔ (componentSet T.F i ∩ closure ↑U).Nonempty

theorem Hironaka.Manifold.BMO.mem_meetingPieces_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {i : ComponentIndex T.F} {x : M.carrier} (hx : x ∈ componentSet T.F i) (hxU : x ∈ U) : i ∈ meetingPieces T U hU

An ambient piece through a point of U meets closure U.

noncomputable def Hironaka.Manifold.BMO.meetingMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Finset T.F.ι

The members having a meeting piece.

Equations

• Hironaka.Manifold.BMO.meetingMembers T U hU = Finset.image Sigma.fst (Hironaka.Manifold.BMO.meetingPieces T U hU)

noncomputable def Hironaka.Manifold.BMO.meetingPiece {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : ComponentIndex T.F

An enumeration of the meeting pieces; these are the pieces of the input family.

Equations

• Hironaka.Manifold.BMO.meetingPiece T U hU c = ↑((Hironaka.Manifold.BMO.meetingPieces T U hU).equivFin.symm c)

theorem Hironaka.Manifold.BMO.meetingPiece_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : meetingPiece T U hU c ∈ meetingPieces T U hU

theorem Hironaka.Manifold.BMO.meetingPiece_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Function.Injective (meetingPiece T U hU)

theorem Hironaka.Manifold.BMO.exists_meetingPiece_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {i : ComponentIndex T.F} (hi : i ∈ meetingPieces T U hU) : ∃ (c : Fin (meetingPieces T U hU).card), meetingPiece T U hU c = i

theorem Hironaka.Manifold.BMO.inclusion_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (U : TopologicalSpace.Opens M.carrier) (x : (M.restrict U).carrier) : (M.inclusion U) x ∈ U

A point of M.restrict U lies in U.

theorem Hironaka.Manifold.BMO.fst_meetingPiece_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : (meetingPiece T U hU c).fst ∈ meetingMembers T U hU

noncomputable def Hironaka.Manifold.BMO.inputFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : PieceFamily (M.restrict U)

The input piece family on M.restrict U: the traces on U of the meeting pieces, in the enumeration meetingPiece; the label of a piece is the position of its member among the members having a meeting piece, sorted in the order of the members; its exponent is the ambient exponent componentExponent, the order of 𝓘 along the component.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMO.inputFamily_nextComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (inputFamily T U hU).nextComp = (meetingPieces T U hU).card

theorem Hironaka.Manifold.BMO.inputFamily_nextLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (inputFamily T U hU).nextLabel = (meetingMembers T U hU).card

theorem Hironaka.Manifold.BMO.inputFamily_piece_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {c : ℕ} (hc : c < (meetingPieces T U hU).card) : (inputFamily T U hU).piece c = ⇑(M.inclusion U) ⁻¹' componentSet T.F (meetingPiece T U hU ⟨c, hc⟩)

theorem Hironaka.Manifold.BMO.inputFamily_piece_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {c : ℕ} (hc : (meetingPieces T U hU).card ≤ c) : (inputFamily T U hU).piece c = ∅

theorem Hironaka.Manifold.BMO.inputFamily_piece {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : (inputFamily T U hU).piece ↑c = ⇑(M.inclusion U) ⁻¹' componentSet T.F (meetingPiece T U hU c)

theorem Hironaka.Manifold.BMO.inputFamily_label_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {c : ℕ} (hc : c < (meetingPieces T U hU).card) : (inputFamily T U hU).label c = ↑(((meetingMembers T U hU).orderIsoOfFin ⋯).symm ⟨(meetingPiece T U hU ⟨c, hc⟩).fst, ⋯⟩)

theorem Hironaka.Manifold.BMO.inputFamily_a_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {c : ℕ} (hc : c < (meetingPieces T U hU).card) : (inputFamily T U hU).a c = componentExponent T.F ⋯ T.I (meetingPiece T U hU ⟨c, hc⟩)

theorem Hironaka.Manifold.BMO.inputFamily_a {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : (inputFamily T U hU).a ↑c = componentExponent T.F ⋯ T.I (meetingPiece T U hU c)

noncomputable def Hironaka.Manifold.BMO.inputEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Fin (inputFamily T U hU).nextLabel ↪o T.F.ι

The members having a meeting piece, sorted, as an order embedding of the labels into the members.

Equations

• Hironaka.Manifold.BMO.inputEmb T U hU = (Hironaka.Manifold.BMO.meetingMembers T U hU).orderEmbOfFin ⋯

theorem Hironaka.Manifold.BMO.range_inputEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Set.range ⇑(inputEmb T U hU) = ↑(meetingMembers T U hU)

theorem Hironaka.Manifold.BMO.inputEmb_label {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (c : Fin (meetingPieces T U hU).card) : (inputEmb T U hU) ⟨(inputFamily T U hU).label ↑c, ⋯⟩ = (meetingPiece T U hU c).fst

The member of the label of a piece is the member of the piece.

theorem Hironaka.Manifold.BMO.fst_meetingPiece_eq_of_label_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {c c' : Fin (meetingPieces T U hU).card} (h : (inputFamily T U hU).label ↑c = (inputFamily T U hU).label ↑c') : (meetingPiece T U hU c).fst = (meetingPiece T U hU c').fst

Pieces with the same label belong to the same member.

theorem Hironaka.Manifold.BMO.inputFamily_realizes {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (inputFamily T U hU).Realizes (T.pullback (M.inclusion U) ⋯).F (inputEmb T U hU)

The input family realises the boundary of the restricted triple through the sorted meeting members: a restricted member is the union of the traces of its meeting components, members without a meeting piece are empty on U, and distinct components of one member are disjoint.

theorem Hironaka.Manifold.BMO.inputFamily_isValid {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) : (inputFamily T U hU).IsValid n m

The input family satisfies the invariants of the combinatorial state for (n, m) when T is in the class BMOClass m (which gives 1 ≤ m).