Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.RescalingRegularity

Regular points under parabolic rescaling #

The affine change of variables transports open neighborhoods, almost-everywhere representatives, and parabolic Hölder bounds in both directions.

source
noncomputable def ESS.rescaleHomeomorph (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) :
CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

The translation and parabolic rescaling homeomorphism on spacetime.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ESS.isRegularPoint_parabolicRescale_iff (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
    CKN.IsRegularPoint (CKN.rescaledSpace r x₀ Ω) (CKN.rescaledTime r t₀ I) (parabolicRescaleVelocity x₀ t₀ r u) z ↔ CKN.IsRegularPoint Ω I u (CKN.scalingParabolic r (x₀, t₀) z)

    Regularity is invariant under the affine parabolic rescaling. The neighborhood convention is that of the CKN regular-point definition.

    source
    theorem ESS.isRegularPoint_parabolicRescale (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (hRegular : CKN.IsRegularPoint Set.univ (Set.Ioi (-(t₀ / r ^ 2))) (parabolicRescaleVelocity x₀ t₀ r u) (0, -(1 / 8))) :
    CKN.IsRegularPoint Set.univ (Set.Ioi 0) u (x₀, t₀ + r ^ 2 * -(1 / 8))

    A regular point of the rescaled global positive-time solution pulls back to the corresponding regular point of the original solution, in the rescaling used by manuscript labels lem:thmA-rescaled and lem:regular-point-shift.