The count of deleted blow-ups

The length of a list after deleting its empty blow-ups plus the number of empty centres is its length (length_eraseEmpty_add_card; the "reindexing" of [Kol07, 34.1]): by recursion, an empty head is deleted and counted once, a nonempty head is kept and not counted, and the transport along the analytic isomorphism of an empty blowing-up keeps the length.

noncomputable def AnalyticManifold.BlowUpSequence.emptyCount {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : ℕ

The number of empty centres of a list.

Equations

• L.emptyCount = {i : Fin L.toSuccession.length | L.toSuccession.IsEmptyAt i}.card

theorem AnalyticManifold.BlowUpSequence.emptyCount_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} : (nil M).emptyCount = 0

theorem AnalyticManifold.BlowUpSequence.emptyCount_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) : (cons hY rest).emptyCount = (if Y = ∅ then 1 else 0) + rest.emptyCount

theorem AnalyticManifold.BlowUpSequence.length_eraseEmpty_add_emptyCount {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.eraseEmpty.length + L.emptyCount = L.length

theorem AnalyticManifold.BlowUpSequence.length_eraseEmpty_add_card {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.eraseEmpty.length + {i : Fin L.toSuccession.length | L.toSuccession.IsEmptyAt i}.card = L.length

[Kol07, 34.1] ("reindexing the resulting blow-up sequence"): the length after deletion plus the number of empty centres is the length (clause on lists).