Finite-time singularity formation for C^{1,α} solutions to the incompressible Euler equations on ℝ³

Problem statement

Notes: Unavailable.

Source: T. M. Elgindi, `Finite-time singularity formation for C^{1,α} solutions to the incompressible Euler equations on ℝ³`, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-3-FiniteTimeSingularity.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 :
    ∃ α > 0, ∃ u₀, div u₀ = 0 ∧ FiniteTimeSingularity.IsOdd u₀ ∧ IsContDiffHolder ℝ α u₀ ∧
      (∃ C > 0, ∀ x, ‖(∇×u₀) x‖ ≤ C / (‖x‖ ^ (α : ℝ) + 1)) ∧
        ∃ p, ∃ u, (∀ t ∈ Ico 0 1, FiniteTimeSingularity.IsOdd (u · t)) ∧
            FiniteTimeSingularity.IsLocalEulerEquationSolution p u₀ 1 u ∧
              (∀ T ∈ Ioo 0 1, IsContDiffHolderOn ℝ α u.uncurry (univ ×ˢ Icc 0 T)) ∧
                Tendsto (fun t ↦ ∫ s in 0..t, ⨆ x, ‖(∇×(u · s)) x‖) (𝓝[<] 1) atTop := by⊢ ∃ α > 0,
  ∃ u₀,
    div u₀ = 0 ∧
      IsOdd u₀ ∧
        IsContDiffHolder ℝ α u₀ ∧
          (∃ C > 0, ∀ (x : ℝ³), ‖(∇×u₀) x‖ ≤ C / (‖x‖ ^ ↑α + 1)) ∧
            ∃ p u,
              (∀ t ∈ Ico 0 1, IsOdd fun x => u x t) ∧
                IsLocalEulerEquationSolution p u₀ 1 u ∧
                  (∀ T ∈ Ioo 0 1, IsContDiffHolderOn ℝ α (Function.uncurry u) (univ ×ˢ Icc 0 T)) ∧
                    Tendsto (fun t => ∫ (s : ℝ) in 0..t, ⨆ x, ‖(∇×fun x => u x s) x‖) (𝓝[<] 1) atTop
  sorryAll goals completed! 🐙