Documentation

LeanPool.EscauriazaSereginSverak.Linear.UCCutoffDerivatives

Derivatives of the Gaussian cutoff #

The spatial and temporal derivatives separate because the Gaussian cutoff is a product of a spatial factor and two time factors.

source
noncomputable def ESS.ucGaussianTimeCutoff (ε s : ℝ) :
ℝ

The combined time factor of the Gaussian cutoff.

Equations
Instances For
    source
    theorem ESS.ucGaussianTimeCutoff_smooth (ε : ℝ) :
    ContDiff ℝ (↑⊤) (ucGaussianTimeCutoff ε)

    The combined time factor is smooth.

    source
    theorem ESS.ucGaussianTimeCutoff_deriv (ε s : ℝ) :
    deriv (ucGaussianTimeCutoff ε) s = deriv ucFinalTimeCutoff s * ucInitialTimeCutoff ε s + ucFinalTimeCutoff s * deriv (ucInitialTimeCutoff ε) s

    The derivative of the combined time cutoff is the sum of its two transition derivatives.

    source
    theorem ESS.ucGaussianTimeCutoff_bounds (ε s : ℝ) :
    0 ≤ ucGaussianTimeCutoff ε s ∧ ucGaussianTimeCutoff ε s ≤ 1

    The combined time cutoff takes values between zero and one.

    source
    theorem ESS.ucGaussianTimeCutoff_abs_deriv_bound {ε : ℝ} (hε : 0 < ε) (s : ℝ) :
    |deriv (ucGaussianTimeCutoff ε) s| ≤ 32 + 8 / ε

    The combined time cutoff has a derivative bound separating the final transition from the initial transition.

    source
    theorem ESS.ucGaussianCutoff_spatialPartial {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) :
    CKN.spatialPartial (ucGaussianCutoff ρ hρ ε) j z = CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) j z * ucGaussianTimeCutoff ε z.2

    The first spatial derivative is carried entirely by the spatial factor.

    source
    theorem ESS.ucGaussianCutoff_spatialSecondPartial {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) :
    CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) i j z = CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) i j z * ucGaussianTimeCutoff ε z.2

    The second spatial derivative is carried entirely by the spatial factor.

    source
    theorem ESS.ucGaussianCutoff_timePartial {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
    CKN.timePartial (ucGaussianCutoff ρ hρ ε) z = ucSpatialCutoff ρ hρ z.1 * deriv (ucGaussianTimeCutoff ε) z.2

    The time derivative is carried entirely by the combined time factor.

    source
    theorem ESS.ucGaussianCutoff_spatialPartial_bound {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) :
    |CKN.spatialPartial (ucGaussianCutoff ρ hρ ε) j z| ≤ CKN.cutoffGradientConstant / ρ

    The first spatial derivatives of the Gaussian cutoff obey the CKN ball cutoff bound.

    source
    theorem ESS.ucGaussianCutoff_spatialSecondPartial_bound {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) :
    |CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) i j z| ≤ CKN.cutoffSecondDerivativeConstant / ρ ^ 2

    The second spatial derivatives of the Gaussian cutoff obey the CKN ball cutoff bound.

    source
    theorem ESS.ucGaussianCutoff_timePartial_bound {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
    |CKN.timePartial (ucGaussianCutoff ρ hρ ε) z| ≤ 32 + 8 / ε

    The time derivative of the Gaussian cutoff is bounded by a final-time constant and the inverse initial transition length.