The monomial phase as a compatible family

The monomial phase at the mark 1 ([Wlo09, Theorem 7.4.1]) in the family form of the library ([Wlo09, Theorem 2.0.3 (4)], [Wlo09, Definition 3.2.6]; [Kol07, 34.1]): on every relatively compact open U of M the value is the complete monomial phase of the restricted triple T|U, the fuel being the measure Σ_D a_D of T|U (Step2bMeasure.lean), finite because the order of 𝓘 is bounded on the compact closure of U (exists_boClass_pullback_inclusion); and the compatibility along U ≤ V is the commutation theorem step2bPhase_pullback_eraseEmpty of Step2bCommute.lean along the open inclusion, the restriction of the restriction being the restriction (pullback_inclusion_restrictLE).

The family has no empty centre (noEmptyCenters_step2bPhase) and its value on every open is of order ≥ 1 for the restricted (𝓘, 1) (step2bFam_isOfOrderGe, from isOfOrderGe_step2bPhase).

Congruence for equal triples

theorem Hironaka.Manifold.BMOmod.step2bPhase_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (k : ℕ) {T₁ T₂ : Manifold.AnalyticTriple ψ₀ M} (e : T₁ = T₂) (h₁ : Manifold.AnalyticTriple.BMOClass 1 T₁) (h₂ : Manifold.AnalyticTriple.BMOClass 1 T₂) : step2bPhase k T₁ h₁ = step2bPhase k T₂ h₂

The phase of equal triples (on the same manifold) is the same list.

theorem Hironaka.Manifold.BMOmod.step2bMeasure_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ M} (e : T₁ = T₂) (h₁ : Manifold.AnalyticTriple.BMOClass 1 T₁) (h₂ : Manifold.AnalyticTriple.BMOClass 1 T₂) : step2bMeasure T₁ h₁ = step2bMeasure T₂ h₂

The measure of equal triples is the same.

The restricted triple: its class and its finite measure

theorem Hironaka.Manifold.BMOmod.bmoClass_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) : Manifold.AnalyticTriple.BMOClass 1 (T.pullback (M.inclusion U) ⋯)

The restriction of a triple of the class to an open is in the class (bmoClass_pullback_inclusion_of_bmoClass).

theorem Hironaka.Manifold.BMOmod.step2bMeasure_restrict_ne_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : step2bMeasure (T.pullback (M.inclusion U) ⋯) ⋯ ≠ ⊤

The measure of the restriction to a relatively compact open is finite: the order of 𝓘 is bounded on the compact closure, so the restricted triple lies in some BO_{n,m} and step2bMeasure_ne_top applies.

noncomputable def Hironaka.Manifold.BMOmod.famFuel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) : ℕ

The fuel of the phase on an open: the measure of the restriction (finite on a relatively compact open, step2bMeasure_restrict_ne_top).

Equations

• Hironaka.Manifold.BMOmod.famFuel T hT U = (Hironaka.Manifold.BMOmod.step2bMeasure (T.pullback (M.inclusion U) ⋯) ⋯).toNat

theorem Hironaka.Manifold.BMOmod.step2bMeasure_restrict_le_famFuel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : step2bMeasure (T.pullback (M.inclusion U) ⋯) ⋯ ≤ ↑(famFuel T hT U)

On a relatively compact open the fuel is at least the measure, so the phase is complete.

The family

noncomputable def Hironaka.Manifold.BMOmod.step2bFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : CompatibleFamily T

The monomial phase as a compatible family ([Wlo09, Theorem 7.4.1] at µ = 1, in the family form of [Wlo09, Theorem 2.0.3 (4)] and [Wlo09, Definition 3.2.6]; the second condition of [Kol07, 34.1]): on every relatively compact open the complete phase of the restricted triple, compatible along open inclusions by the commutation theorem.

Equations

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

theorem Hironaka.Manifold.BMOmod.step2bFam_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (step2bFam T hT).seqOn U hU = step2bPhase (famFuel T hT U) (T.pullback (M.inclusion U) ⋯) ⋯

The family's value on an open is the complete phase of the restricted triple.

theorem Hironaka.Manifold.BMOmod.step2bFam_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((step2bFam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The order clause at the mark 1 for the monomial phase: the value on every open is of order ≥ 1 for the restricted (𝓘, 1) (isOfOrderGe_step2bPhase).