The order-reduction tower at the library's constructions

The order-reduction tower on the compatible-family structures (Stage/Family.lean) takes the two reduction steps of [Kol07, 70] as parameters. This module instantiates it at the steps the library constructs, over any field K with RCLike K: Theorem 103 as theorem103FamStar (Stage/InstancesFam.lean), and Theorem 107 as theorem107FamStarOf (Stage/InstancesFamTheorem107.lean) applied to the monomial procedure BMO.monomialStep3Fam of Step 3 of the proof of Theorem 107 (BMO/Step3Monomial/Functor.lean) and to the two transform identities for the nonmonomial part proved in Modified/NonmonomialTransformMod.lean.

• nonmonomialTransformIdentity_refl K n — the transform identity for the nonmonomial part at the standard model of dimension n;
• concreteTheorem107FamStar K : BMOanFamStep K — Theorem 107 as the second reduction step, at the library's constructions;
• concreteOrderReductionTower K n — the tower along the two steps;
• concreteBOanFam K n d : BOanFam K n d — order reduction for ideals in every dimension and at every mark ([Kol07, Theorem 68]), and concreteBMOanFam K n : BMOanFam K n 1 — order reduction for marked ideals at the mark 1 ([Kol07, Theorem 69]), both read off the tower;
• concreteBOanFamReal n m : BOanFam ℝ n m — the same order-reduction family over ℝ, written as BOanFamAllOf at the second step.

These are the order-reduction functors the analytic main theorems apply: concreteBOanFam and concreteBMOanFam enter the embedded desingularization (Hironaka/Resolution/Analytic/Wlo09/Concrete.lean).

theorem Hironaka.nonmonomialTransformIdentity_refl (K : Type) [RCLike K] (n : ℕ) : Manifold.BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl K (Fin n → K))

The transform identity for the nonmonomial part (BMOmod.NonmonomialTransformIdentity) at the standard model Fin n → K of every dimension: nonmonomialTransformIdentity_inhabitant at that model.

noncomputable def Hironaka.concreteTheorem107FamStar (K : Type) [RCLike K] : Manifold.BMOanFamStep K

Order reduction for marked ideals from order reduction for ideals in the same dimension ([Kol07, Theorem 107]), as the second reduction step of the tower: theorem107FamStarOf at the monomial procedure BMO.monomialStep3Fam and the two transform identities for the nonmonomial part, in every dimension.

Equations

• Hironaka.concreteTheorem107FamStar K = Hironaka.Manifold.theorem107FamStarOf K (fun (n m : ℕ) => Hironaka.Manifold.BMO.monomialStep3Fam K n m) ⋯ ⋯

noncomputable def Hironaka.concreteOrderReductionTower (K : Type) [RCLike K] (n : ℕ) : Manifold.OrderReductionStageAnFam K n

The order-reduction tower on the compatible-family structures along Theorem 103 (theorem103FamStar) and Theorem 107 (concreteTheorem107FamStar).

Equations

• Hironaka.concreteOrderReductionTower K = Hironaka.Manifold.orderReductionTowerAnFamStarOf K (Hironaka.concreteTheorem107FamStar K)

noncomputable def Hironaka.concreteBOanFam (K : Type) [RCLike K] (n d : ℕ) : Manifold.BOanFam K n d

Order reduction for ideals in dimension n at the mark d ([Kol07, Theorem 68]), in the compatible-family form: the component bo of the tower concreteOrderReductionTower.

Equations

• Hironaka.concreteBOanFam K n d = (Hironaka.concreteOrderReductionTower K n).bo d

noncomputable def Hironaka.concreteBMOanFam (K : Type) [RCLike K] (n : ℕ) : Manifold.BMOanFam K n 1

Order reduction for marked ideals in dimension n at the mark 1 ([Kol07, Theorem 69]), in the compatible-family form: the component bmo of the tower concreteOrderReductionTower at the mark 1.

Equations

• Hironaka.concreteBMOanFam K n = (Hironaka.concreteOrderReductionTower K n).bmo 1

noncomputable def Hironaka.concreteBOanFamReal (n m : ℕ) : Manifold.BOanFam ℝ n m

Order reduction for ideals over ℝ in dimension n at the mark m, in the compatible-family form: BOanFamAllOf at the second reduction step theorem107FamStarOf applied to the library's constructions, which unfolds to concreteBOanFam ℝ n m.

Equations

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