Documentation

LeanPool.EscauriazaSereginSverak.Linear.UCInitialErrorGeometry

Spatial scale of the initial time transition #

A quarter-power spatial radius contains the transition time interval while shrinking toward the flatness center.

theorem ESS.uc_initial_error_fourth_root_geometry {ρ ε : ℝ} (hρ : 4 ≤ ρ) (hε : 0 < ε) (hεsmall : ε < 1 / 4) :
have r := √√ε; 0 < r ∧ r < ρ ∧ r ^ 4 = ε ∧ 2 * ε < r ^ 2

The fourth-root spatial scale is larger than the parabolic time scale of the initial transition.