Spatial Cutoffs

Gevrey Cutoff

noncomputable def EulerGevreyCutoff.complexFlat (z : ℂ) : ℂ

Holomorphic function used to estimate the flat real bump by Cauchy's inequality.

Equations

• EulerGevreyCutoff.complexFlat z = Complex.exp (-z⁻¹)

theorem EulerGevreyCutoff.real_part_inv_lower_bound (x : ℝ) (hx : 0 < x) (z : ℂ) (hz : ‖z - ↑x‖ ≤ x / 2) : 1 / (8 * x) ≤ z⁻¹.re

theorem EulerGevreyCutoff.complexFlat_differentiableAt {z : ℂ} (hz : z ≠ 0) : DifferentiableAt ℂ complexFlat z

theorem EulerGevreyCutoff.complexFlat_disc_bound (x : ℝ) (hx : 0 < x) (z : ℂ) (hz : ‖z - ↑x‖ ≤ x / 2) : ‖complexFlat z‖ ≤ Real.exp (-(1 / (8 * x)))

theorem EulerGevreyCutoff.factorial_decay (n : ℕ) (t : ℝ) (ht : 0 ≤ t) : t ^ n * Real.exp (-t) ≤ ↑n.factorial

theorem EulerGevreyCutoff.complexFlat_gevrey_bound (n : ℕ) (x : ℝ) (hx : 0 < x) : ‖iteratedDeriv n complexFlat ↑x‖ ≤ 16 ^ n * ↑n.factorial ^ 2

theorem EulerGevreyCutoff.iteratedDeriv_real_restriction (f : ℂ → ℂ) (s : Set ℂ) (hs : IsOpen s) (hf : DifferentiableOn ℂ f s) (n : ℕ) (x : ℝ) (hx : ↑x ∈ s) : iteratedDeriv n (fun (t : ℝ) => (f ↑t).re) x = (iteratedDeriv n f ↑x).re

theorem EulerGevreyCutoff.polynomial_glue_flat (p : Polynomial ℝ) (n : ℕ) (x : ℝ) (hx : x ≤ 0) : iteratedDeriv n (fun (y : ℝ) => Polynomial.eval y⁻¹ p * expNegInvGlue y) x = 0

theorem EulerGevreyCutoff.expNegInvGlue_gevrey_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n expNegInvGlue x| ≤ 16 ^ n * ↑n.factorial ^ 2

noncomputable def EulerGevreyCutoff.rawBump (x : ℝ) : ℝ

Nonnegative even smooth bump supported on the unit interval.

Equations

• EulerGevreyCutoff.rawBump x = expNegInvGlue (x + 1) * expNegInvGlue (1 - x)

theorem EulerGevreyCutoff.rawBump_contDiff : ContDiff ℝ (↑⊤) rawBump

theorem EulerGevreyCutoff.rawBump_nonneg (x : ℝ) : 0 ≤ rawBump x

theorem EulerGevreyCutoff.rawBump_even (x : ℝ) : rawBump (-x) = rawBump x

theorem EulerGevreyCutoff.rawBump_pos_zero : 0 < rawBump 0

theorem EulerGevreyCutoff.rawBump_support : tsupport rawBump ⊆ Set.Icc (-1) 1

theorem EulerGevreyCutoff.rawBump_compactSupport : HasCompactSupport rawBump

theorem EulerGevreyCutoff.rawBump_gevrey_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n rawBump x| ≤ 3 * 16 ^ n * ↑n.factorial ^ 2

noncomputable def EulerGevreyCutoff.bumpMass : ℝ

Positive integral used to normalize the smooth transition.

Equations

• EulerGevreyCutoff.bumpMass = ∫ (t : ℝ) in -1..1, EulerGevreyCutoff.rawBump t

theorem EulerGevreyCutoff.bumpMass_pos : 0 < bumpMass

noncomputable def EulerGevreyCutoff.transition (x : ℝ) : ℝ

Smooth monotone transition from zero to one, with explicit Gevrey bounds.

Equations

• EulerGevreyCutoff.transition x = (∫ (t : ℝ) in -1..x, EulerGevreyCutoff.rawBump t) / EulerGevreyCutoff.bumpMass

theorem EulerGevreyCutoff.transition_hasDerivAt (x : ℝ) : HasDerivAt transition (rawBump x / bumpMass) x

theorem EulerGevreyCutoff.transition_deriv : deriv transition = fun (x : ℝ) => rawBump x / bumpMass

theorem EulerGevreyCutoff.transition_contDiff : ContDiff ℝ (↑⊤) transition

theorem EulerGevreyCutoff.rawBump_eq_zero_of_le (x : ℝ) (hx : x ≤ -1) : rawBump x = 0

theorem EulerGevreyCutoff.rawBump_eq_zero_of_ge (x : ℝ) (hx : 1 ≤ x) : rawBump x = 0

theorem EulerGevreyCutoff.transition_zero_of_le (x : ℝ) (hx : x ≤ -1) : transition x = 0

theorem EulerGevreyCutoff.transition_one_of_ge (x : ℝ) (hx : 1 ≤ x) : transition x = 1

theorem EulerGevreyCutoff.transition_monotone : Monotone transition

theorem EulerGevreyCutoff.transition_mem_unitInterval (x : ℝ) : transition x ∈ Set.Icc 0 1

theorem EulerGevreyCutoff.transition_gevrey_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n transition x| ≤ (1 + 3 / bumpMass) * 16 ^ n * ↑n.factorial ^ 2

noncomputable def EulerSpatialCutoffs.normalizedBump (t : ℝ) : ℝ

The even one-dimensional bump normalized to have value one at the origin.

Equations

• EulerSpatialCutoffs.normalizedBump t = EulerGevreyCutoff.rawBump t / EulerGevreyCutoff.rawBump 0

theorem EulerSpatialCutoffs.normalizedBump_contDiff : ContDiff ℝ (↑⊤) normalizedBump

theorem EulerSpatialCutoffs.normalizedBump_zero : normalizedBump 0 = 1

theorem EulerSpatialCutoffs.normalizedBump_even (t : ℝ) : normalizedBump (-t) = normalizedBump t

theorem EulerSpatialCutoffs.normalizedBump_nonneg (t : ℝ) : 0 ≤ normalizedBump t

theorem EulerSpatialCutoffs.normalizedBump_gevrey (n : ℕ) (t : ℝ) : |iteratedDeriv n normalizedBump t| ≤ 3 / EulerGevreyCutoff.rawBump 0 * EulerGevrey.majorant 16 0 n

noncomputable def EulerSpatialCutoffs.outerWindow (t : ℝ) : ℝ

A plateau on the unit interval with support inside the interval of radius nine eighths.

Equations

• EulerSpatialCutoffs.outerWindow t = EulerGevreyCutoff.transition (17 + 16 * t) * EulerGevreyCutoff.transition (17 - 16 * t)

theorem EulerSpatialCutoffs.outerWindow_contDiff : ContDiff ℝ (↑⊤) outerWindow

theorem EulerSpatialCutoffs.outerWindow_even (t : ℝ) : outerWindow (-t) = outerWindow t

theorem EulerSpatialCutoffs.outerWindow_one (t : ℝ) (ht : |t| ≤ 1) : outerWindow t = 1

theorem EulerSpatialCutoffs.outerWindow_zero (t : ℝ) (ht : 9 / 8 ≤ |t|) : outerWindow t = 0

theorem EulerSpatialCutoffs.outerWindow_gevrey (n : ℕ) (t : ℝ) : |iteratedDeriv n outerWindow t| ≤ 3 * (1 + 3 / EulerGevreyCutoff.bumpMass) ^ 2 * EulerGevrey.majorant 256 0 n

def EulerSpatialCutoffs.tensorCutoff (g : ℝ → ℝ) (a : ℝ) (x : EulerSmoothLimit.Space) : ℝ

Product of three copies of a scalar profile at a common coordinate scale.

Equations

• EulerSpatialCutoffs.tensorCutoff g a x = ∏ i : Fin 3, g (a * x.ofLp i)

theorem EulerSpatialCutoffs.tensorCutoff_contDiff (g : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) (a : ℝ) : ContDiff ℝ (↑⊤) (tensorCutoff g a)

theorem EulerSpatialCutoffs.tensorCutoff_even (g : ℝ → ℝ) (hg : ∀ (t : ℝ), g (-t) = g t) (a : ℝ) (x : EulerSmoothLimit.Space) : tensorCutoff g a (-x) = tensorCutoff g a x

theorem EulerSpatialCutoffs.tensorCutoff_gevrey (g : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) (a R A : ℝ) (ha : 0 ≤ a) (hR : 0 ≤ R) (hA : 0 ≤ A) (hb : ∀ (n : ℕ) (t : ℝ), |iteratedDeriv n g t| ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (tensorCutoff g a) x‖ ≤ (3 * A) ^ 3 * EulerGevrey.majorant (R * a) 0 n

noncomputable def EulerSpatialCutoffs.innerCutoff : EulerSmoothLimit.Space → ℝ

Inner spatial cutoff used to localize the leading oscillatory packet.

Equations

• EulerSpatialCutoffs.innerCutoff = EulerSpatialCutoffs.tensorCutoff EulerSpatialCutoffs.normalizedBump 4

noncomputable def EulerSpatialCutoffs.outerCutoff : EulerSmoothLimit.Space → ℝ

Outer plateau used by the compactly supported mean correction.

Equations

• EulerSpatialCutoffs.outerCutoff = EulerSpatialCutoffs.tensorCutoff EulerSpatialCutoffs.outerWindow 1

theorem EulerSpatialCutoffs.innerCutoff_contDiff : ContDiff ℝ (↑⊤) innerCutoff

theorem EulerSpatialCutoffs.outerCutoff_contDiff : ContDiff ℝ (↑⊤) outerCutoff

theorem EulerSpatialCutoffs.innerCutoff_even (x : EulerSmoothLimit.Space) : innerCutoff (-x) = innerCutoff x

theorem EulerSpatialCutoffs.outerCutoff_even (x : EulerSmoothLimit.Space) : outerCutoff (-x) = outerCutoff x

theorem EulerSpatialCutoffs.innerCutoff_nonneg (x : EulerSmoothLimit.Space) : 0 ≤ innerCutoff x

theorem EulerSpatialCutoffs.innerCutoff_zero : innerCutoff 0 = 1

theorem EulerSpatialCutoffs.outerCutoff_one (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ 1) : outerCutoff x = 1

theorem EulerSpatialCutoffs.innerCutoff_gevrey (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n innerCutoff x‖ ≤ (9 / EulerGevreyCutoff.rawBump 0) ^ 3 * EulerGevrey.majorant 64 0 n

theorem EulerSpatialCutoffs.outerCutoff_gevrey (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n outerCutoff x‖ ≤ (9 * (1 + 3 / EulerGevreyCutoff.bumpMass) ^ 2) ^ 3 * EulerGevrey.majorant 256 0 n

theorem EulerSpatialCutoffs.cube_closed (r : ℝ) : IsClosed {x : EulerSmoothLimit.Space | ∀ (i : Fin 3), |x.ofLp i| ≤ r}

theorem EulerSpatialCutoffs.norm_sq_le_of_mem_cube (r : ℝ) (hr : 0 ≤ r) (x : EulerSmoothLimit.Space) (hx : x ∈ {x : EulerSmoothLimit.Space | ∀ (i : Fin 3), |x.ofLp i| ≤ r}) : ‖x‖ ^ 2 ≤ 3 * r ^ 2

theorem EulerSpatialCutoffs.tensorCutoff_support (g : ℝ → ℝ) (a b : ℝ) (ha : 0 < a) (hg : ∀ (t : ℝ), g t ≠ 0 → |t| ≤ b) : tsupport (tensorCutoff g a) ⊆ {x : EulerSmoothLimit.Space | ∀ (i : Fin 3), |x.ofLp i| ≤ b / a}

theorem EulerSpatialCutoffs.innerCutoff_support : tsupport innerCutoff ⊆ Metric.ball 0 (1 / 2)

theorem EulerSpatialCutoffs.outerCutoff_support : tsupport outerCutoff ⊆ Metric.closedBall 0 2

theorem EulerSpatialCutoffs.innerCutoff_compactSupport : HasCompactSupport innerCutoff

theorem EulerSpatialCutoffs.outerCutoff_compactSupport : HasCompactSupport outerCutoff