The rounds on the nonmonomial part: compatibility and independence of the value

The compatibility of the values on relatively compact opens ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]; [Kol07, 34.1]) for the rounds on the nonmonomial part: the value on U ≤ V is the value on V restricted to U and cleaned of empty blow-ups (stepAFamOn_compat). The independence of the value from the outer open on which the bound was read is proved by the same device in StepAIndep.lean (stepAFamOnAux_eq, stepAFamOn_eq_of_outer).

Both are the alignment of two descents (descentStateAux_rel) through a third, virtual descent for the triple pulled back along the identity: its chain is the intersection of the two chains (joinChain for the chains of two compact sets in two outer opens, stepAJoin for the canonical chains: relatively compact, shrinking, containing closure U), its bound the larger of the two bounds (the index of the canonical exhaustion open is a choice, so the two bounds are not comparable a priori). Aligned with either descent, the final list of the virtual descent restricted to U is the final list of that descent restricted to U, up to empty blow-ups (descent_restrict_eq, descentValueAt_eq_join_left, descentValueAt_eq_join_right); hence the two values agree.

The triple pulled back along the identity

theorem Hironaka.Manifold.BMOmod.bmoClass_pullback_id {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) : Manifold.AnalyticTriple.BMOClass m (T.pullback ContMDiffMap.id ⋯)

The marked class passes to the triple pulled back along the identity (the triple of the virtual descent).

A descent restricted to a smaller open, through the virtual descent

theorem Hironaka.Manifold.BMOmod.descent_restrict_eq {𝕜 : 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) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (r : ℕ) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (D : ℕ) (hD : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D) (X : ℕ → TopologicalSpace.Opens M.carrier) (hX : ∀ (j : ℕ), IsCompact (closure ↑(X j))) (rX : ℕ) (hXsub : ∀ j < rX, closure ↑(X (j + 1)) ⊆ ↑(X j)) (DX : ℕ) (hDX : ∀ x ∈ ↑(X 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple (T.pullback ContMDiffMap.id ⋯)).I x ≤ ↑DX) (hDD : D ≤ DX) (hrr : rX ≤ DX - D + r) (hXW : ∀ (j : ℕ), X j ≤ W (j - (DX - D))) (hrXt : rX ≤ DX + 1 - t) {U' : TopologicalSpace.Opens M.carrier} (hU'X : U' ≤ X rX) : ((descentStateAux T m hT bo ⋯ ⋯ t hm hmt W hW r hWsub D hD (rX - (DX - D)) ⋯ ⋯).L.pullback (M.restrictLE ⋯) ⋯).eraseEmpty = ((descentStateAux (T.pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt X hX rX hXsub DX hDX rX ⋯ hrXt).L.pullback (M.restrictLE hU'X) ⋯).eraseEmpty

A descent restricted to a smaller open equals the virtual descent restricted there, up to empty blow-ups: the alignment descentStateAux_rel along the identity, then the restriction to U' composed with the inclusion (eraseEmpty_pullback_eraseEmpty, pullback_comp).

The value with the bound as a parameter

noncomputable def Hironaka.Manifold.BMOmod.valueAt {𝕜 : 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) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (D : ℕ) (hWsub : ∀ k < D + 1 - t, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hD : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D) (k : ℕ) (hk : k ≤ D + 1 - t) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ W k) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U')

The final list of the descent along W from the bound D after k links, restricted to an open U' ≤ W k and cleaned of empty blow-ups, with the bound as an explicit parameter (its type does not depend on D or k).

Equations

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

theorem Hironaka.Manifold.BMOmod.valueAt_congr {𝕜 : 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) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) {D D' k k' : ℕ} (eD : D = D') (ek : k = k') (hWsub : ∀ k < D + 1 - t, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hD : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D) (hk : k ≤ D + 1 - t) (hWsub' : ∀ k < D' + 1 - t, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hD' : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D') (hk' : k' ≤ D' + 1 - t) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ W k) (hU'k' : U' ≤ W k') : valueAt T m hT bo ⋯ ⋯ t hm hmt W hW D hWsub hD k hk hU'k = valueAt T m hT bo ⋯ ⋯ t hm hmt W hW D' hWsub' hD' k' hk' hU'k'

valueAt depends on the bound and the index only through their values (a substitution).

Descents along the chains of a compact set, and their virtual join

theorem Hironaka.Manifold.BMOmod.sub_links_eq {DU DX t : ℕ} (h : DU ≤ DX) : DU + 1 - t = DX + 1 - t - (DX - DU)

The number of links of a descent from the smaller bound DU ≤ DX is the number of links of the descent from DX past its first DX − DU links.

theorem Hironaka.Manifold.BMOmod.links_le_sub_add {DU DX t : ℕ} (h : DU ≤ DX) : DX + 1 - t ≤ DX - DU + (DU + 1 - t)

The descent from DX is no longer than its first DX − DU links plus the descent from DU.

theorem Hironaka.Manifold.BMOmod.shrinkChain_zero_bound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (K : Set M.carrier) (hK : IsCompact K) (O : TopologicalSpace.Opens M.carrier) (hO : IsCompact (closure ↑O)) (hKO : K ⊆ ↑O) (x : M.carrier) (hx : x ∈ ↑(shrinkChain K O hK hKO 0)) : Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑(BMO.roundOrderOn T O)

The bound on the first open of the chain of K inside O is roundOrderOn T O.

noncomputable def Hironaka.Manifold.BMOmod.descentValueAt {𝕜 : 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) (K : Set M.carrier) (hK : IsCompact K) (O : TopologicalSpace.Opens M.carrier) (hO : IsCompact (closure ↑O)) (hKO : K ⊆ ↑O) (k : ℕ) (hk : k ≤ BMO.roundOrderOn T O + 1 - t) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ shrinkChain K O hK hKO k) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U')

The final list of the descent of K inside O after k links, restricted to U' ≤ W k and cleaned of empty blow-ups (its type does not depend on k).

Equations

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

theorem Hironaka.Manifold.BMOmod.descentValueAt_congr {𝕜 : 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) (K : Set M.carrier) (hK : IsCompact K) (O : TopologicalSpace.Opens M.carrier) (hO : IsCompact (closure ↑O)) (hKO : K ⊆ ↑O) {k k' : ℕ} (e : k = k') (hk : k ≤ BMO.roundOrderOn T O + 1 - t) (hk' : k' ≤ BMO.roundOrderOn T O + 1 - t) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ shrinkChain K O hK hKO k) (hU'k' : U' ≤ shrinkChain K O hK hKO k') : descentValueAt T m hT bo ⋯ ⋯ t hm hmt K hK O hO hKO k hk hU'k = descentValueAt T m hT bo ⋯ ⋯ t hm hmt K hK O hO hKO k' hk' hU'k'

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.joinChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (j : ℕ) : TopologicalSpace.Opens M.carrier

The intersection of the two chains.

Equations

• Hironaka.Manifold.BMOmod.joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ j = Hironaka.Manifold.shrinkChain K₁ O₁ hK₁ hK₁O₁ j ⊓ Hironaka.Manifold.shrinkChain K₂ O₂ hK₂ hK₂O₂ j

theorem Hironaka.Manifold.BMOmod.isCompact_closure_joinChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (j : ℕ) : IsCompact (closure ↑(joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ j))

theorem Hironaka.Manifold.BMOmod.closure_joinChain_succ_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (j : ℕ) : closure ↑(joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ (j + 1)) ⊆ ↑(joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ j)

theorem Hironaka.Manifold.BMOmod.joinChain_le_left {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (j k : ℕ) (hkj : k ≤ j) : joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ j ≤ shrinkChain K₁ O₁ hK₁ hK₁O₁ k

theorem Hironaka.Manifold.BMOmod.joinChain_le_right {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (j k : ℕ) (hkj : k ≤ j) : joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ j ≤ shrinkChain K₂ O₂ hK₂ hK₂O₂ k

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.joinBound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (O₁ O₂ : TopologicalSpace.Opens M.carrier) : ℕ

The larger of the two bounds.

Equations

• Hironaka.Manifold.BMOmod.joinBound T O₁ O₂ = max (Hironaka.Manifold.BMO.roundOrderOn T O₁) (Hironaka.Manifold.BMO.roundOrderOn T O₂)

theorem Hironaka.Manifold.BMOmod.joinChain_bound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hO₁ : IsCompact (closure ↑O₁)) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) (x : M.carrier) (hx : x ∈ ↑(joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ 0)) : Manifold.IdealSheaf.ord (BMO.nonmonomialTriple (T.pullback ContMDiffMap.id ⋯)).I x ≤ ↑(joinBound T O₁ O₂)

theorem Hironaka.Manifold.BMOmod.descentValueAt_eq_join_left {𝕜 : 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) (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hO₁ : IsCompact (closure ↑O₁)) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hK₂O₂ : K₂ ⊆ ↑O₂) {U' : TopologicalSpace.Opens M.carrier} (hU' : U' ≤ joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ (joinBound T O₁ O₂ + 1 - t)) : descentValueAt T m hT bo ⋯ ⋯ t hm hmt K₁ hK₁ O₁ hO₁ hK₁O₁ (BMO.roundOrderOn T O₁ + 1 - t) ⋯ ⋯ = ((descentStateAux (T.pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂) ⋯ (joinBound T O₁ O₂ + 1 - t) ⋯ (joinBound T O₁ O₂) ⋯ (joinBound T O₁ O₂ + 1 - t) ⋯ ⋯).L.pullback (M.restrictLE hU') ⋯).eraseEmpty

The descent of the first chain, aligned with the virtual descent and restricted to an open U' inside the last open of the virtual chain.

theorem Hironaka.Manifold.BMOmod.descentValueAt_eq_join_right {𝕜 : 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) (K₁ : Set M.carrier) (hK₁ : IsCompact K₁) (O₁ : TopologicalSpace.Opens M.carrier) (hO₁ : IsCompact (closure ↑O₁)) (hK₁O₁ : K₁ ⊆ ↑O₁) (K₂ : Set M.carrier) (hK₂ : IsCompact K₂) (O₂ : TopologicalSpace.Opens M.carrier) (hO₂ : IsCompact (closure ↑O₂)) (hK₂O₂ : K₂ ⊆ ↑O₂) {U' : TopologicalSpace.Opens M.carrier} (hU' : U' ≤ joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂ (joinBound T O₁ O₂ + 1 - t)) : descentValueAt T m hT bo ⋯ ⋯ t hm hmt K₂ hK₂ O₂ hO₂ hK₂O₂ (BMO.roundOrderOn T O₂ + 1 - t) ⋯ ⋯ = ((descentStateAux (T.pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (joinChain K₁ hK₁ O₁ hK₁O₁ K₂ hK₂ O₂ hK₂O₂) ⋯ (joinBound T O₁ O₂ + 1 - t) ⋯ (joinBound T O₁ O₂) ⋯ (joinBound T O₁ O₂ + 1 - t) ⋯ ⋯).L.pullback (M.restrictLE hU') ⋯).eraseEmpty

The descent of the second chain, aligned with the virtual descent and restricted to an open U'.

The virtual chain of two canonical chains

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepAJoin {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (j : ℕ) : TopologicalSpace.Opens M.carrier

The intersection of the canonical chains of U and of V: a shrinking chain of relatively compact opens containing closure U ∩ closure V (joinChain of the two canonical chains).

Equations

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

theorem Hironaka.Manifold.BMOmod.isCompact_closure_stepAJoin {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (j : ℕ) : IsCompact (closure ↑(stepAJoin U hU V hV j))

theorem Hironaka.Manifold.BMOmod.closure_stepAJoin_succ_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (j : ℕ) : closure ↑(stepAJoin U hU V hV (j + 1)) ⊆ ↑(stepAJoin U hU V hV j)

theorem Hironaka.Manifold.BMOmod.stepAJoin_le_left {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (j k : ℕ) (hkj : k ≤ j) : stepAJoin U hU V hV j ≤ stepAChainOpens U hU k

theorem Hironaka.Manifold.BMOmod.stepAJoin_le_right {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (j k : ℕ) (hkj : k ≤ j) : stepAJoin U hU V hV j ≤ stepAChainOpens V hV k

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepAJoinBound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) : ℕ

The larger of the two bounds.

Equations

• Hironaka.Manifold.BMOmod.stepAJoinBound T U hU V hV = Hironaka.Manifold.BMOmod.joinBound T (Hironaka.Manifold.BMOmod.stepAOuter U hU) (Hironaka.Manifold.BMOmod.stepAOuter V hV)

theorem Hironaka.Manifold.BMOmod.stepAJoin_bound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (x : M.carrier) (hx : x ∈ ↑(stepAJoin U hU V hV 0)) : Manifold.IdealSheaf.ord (BMO.nonmonomialTriple (T.pullback ContMDiffMap.id ⋯)).I x ≤ ↑(stepAJoinBound T U hU V hV)

The larger bound holds on the first open of the virtual chain, for the triple pulled back along the identity.

The value with a re-indexed final state

noncomputable def Hironaka.Manifold.BMOmod.stepAValueAt {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (k : ℕ) (hk : k ≤ stepALinks T t U hU) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ stepAChainOpens U hU k) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U')

The final list of the canonical descent of U after k links, restricted to an open U' and cleaned of empty blow-ups (its type does not depend on k).

Equations

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

theorem Hironaka.Manifold.BMOmod.stepAValueAt_congr {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {k k' : ℕ} (e : k = k') (hk : k ≤ stepALinks T t U hU) (hk' : k' ≤ stepALinks T t U hU) {U' : TopologicalSpace.Opens M.carrier} (hU'k : U' ≤ stepAChainOpens U hU k) (hU'k' : U' ≤ stepAChainOpens U hU k') : stepAValueAt T m hT bo ⋯ ⋯ t hm hmt U hU k hk hU'k = stepAValueAt T m hT bo ⋯ ⋯ t hm hmt U hU k' hk' hU'k'

theorem Hironaka.Manifold.BMOmod.stepAFamOn_eq_stepAValueAt {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : stepAFamOn T m hT bo ⋯ ⋯ t hm hmt U hU = stepAValueAt T m hT bo ⋯ ⋯ t hm hmt U hU (stepALinks T t U hU) ⋯ ⋯

The value on U is the final list restricted to U (by definition).

theorem Hironaka.Manifold.BMOmod.stepAFamOn_pullback_eraseEmpty_eq {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : ((stepAFamOn T m hT bo ⋯ ⋯ t hm hmt V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty = stepAValueAt T m hT bo ⋯ ⋯ t hm hmt V hV (stepALinks T t V hV) ⋯ ⋯

The value on V restricted to U ≤ V and cleaned is the final list restricted to U (eraseEmpty_pullback_eraseEmpty, pullback_comp).

Compatibility

theorem Hironaka.Manifold.BMOmod.stepAValueAt_eq_join_left {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) {U' : TopologicalSpace.Opens M.carrier} (hU'U : U' ≤ U) (hU'V : U' ≤ V) : stepAValueAt T m hT bo ⋯ ⋯ t hm hmt U hU (stepALinks T t U hU) ⋯ ⋯ = ((descentStateAux (T.pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (stepAJoin U hU V hV) ⋯ (stepAJoinBound T U hU V hV + 1 - t) ⋯ (stepAJoinBound T U hU V hV) ⋯ (stepAJoinBound T U hU V hV + 1 - t) ⋯ ⋯).L.pullback (M.restrictLE ⋯) ⋯).eraseEmpty

The canonical descent of U, aligned with the virtual descent of the pair U, V and restricted to an open U' ≤ U (descentValueAt_eq_join_left at the canonical chains).

theorem Hironaka.Manifold.BMOmod.stepAValueAt_eq_join_right {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) {U' : TopologicalSpace.Opens M.carrier} (hU'U : U' ≤ U) (hU'V : U' ≤ V) : stepAValueAt T m hT bo ⋯ ⋯ t hm hmt V hV (stepALinks T t V hV) ⋯ ⋯ = ((descentStateAux (T.pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (stepAJoin U hU V hV) ⋯ (stepAJoinBound T U hU V hV + 1 - t) ⋯ (stepAJoinBound T U hU V hV) ⋯ (stepAJoinBound T U hU V hV + 1 - t) ⋯ ⋯).L.pullback (M.restrictLE ⋯) ⋯).eraseEmpty

The canonical descent of V, aligned with the virtual descent of the pair U, V and restricted to an open U' ≤ U (descentValueAt_eq_join_right at the canonical chains).

theorem Hironaka.Manifold.BMOmod.stepAFamOn_compat {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : stepAFamOn T m hT bo ⋯ ⋯ t hm hmt U hU = ((stepAFamOn T m hT bo ⋯ ⋯ t hm hmt V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The compatibility of the values of the rounds ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]; [Kol07, 34.1]): the value on U ≤ V is the value on V restricted to U and cleaned of empty blow-ups. Both are the virtual descent of the pair restricted to U (stepAValueAt_eq_join_left, stepAValueAt_eq_join_right).