Symplectic monodromy at radius zero and equimultiplicity of μ-constant families

Problem statement

Notes: Unavailable.

Source: J. Fernández de Bobadilla and T. Pełka, `Symplectic monodromy at radius zero and equimultiplicity of μ-constant families`, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-200-1-SymplecticMonodromy.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (n : ℕ) (f : unitInterval → MvPowerSeries (Fin n) ℂ)
    (cont : ∀ d, Continuous fun t ↦ coeff d (f t)) (h_const : ∀ t, constantCoeff (f t) = 0)
    (h : ∃ μ : ℕ, ∀ t, milnorNumber (f t) = μ) : ∀ t₁ t₂, (f t₁).order = (f t₂).order := byn:ℕf:↑unitInterval → MvPowerSeries (Fin n) ℂcont:∀ (d : Fin n →₀ ℕ), Continuous fun t => (coeff d) (f t)h_const:∀ (t : ↑unitInterval), constantCoeff (f t) = 0h:∃ μ, ∀ (t : ↑unitInterval), milnorNumber (f t) = ↑μ⊢ ∀ (t₁ t₂ : ↑unitInterval), (f t₁).order = (f t₂).order
  sorryAll goals completed! 🐙