A cutoff at the axis of the lifted variables, and the residual integrand

The residual of eq:aniso:zoom:finite:limit against a test function is split, in the passage to the limit of Step 2 of the proof of prop:aniso:small (deviation D17), into a part supported near the axis X = 0 of the lifted variables and a part supported off it. The splitting uses the smooth cutoff finAxisCutoff ε (X, Z, τ) = b(X / ε), with b a fixed bump equal to 1 on the unit ball and vanishing outside the ball of radius 2 (sup norm on the four radial coordinates). Its j-th derivative is O(ε^{-j}) (norm_iteratedFDeriv_finAxisCutoff_le).

The residual integrand -∂_τ ψ - B · ∇ψ - d ψ - Δ_X ψ is bounded by the first two derivatives of ψ (abs_residualIntegrand_le) and is additive in ψ (residualIntegrand_add).

The cutoff

def CIV.finAxisProj : CKN.Vec 5 × ℝ →L[ℝ] CKN.Vec 5

The projection (X, Z, τ) ↦ (X, 0) onto the four radial coordinates.

Equations

• CIV.finAxisProj = ContinuousLinearMap.pi fun (j : Fin 5) => if j = 4 then 0 else ContinuousLinearMap.proj j ∘SL ContinuousLinearMap.fst ℝ (CKN.Vec 5) ℝ

theorem CIV.finAxisProj_apply (z : CKN.Vec 5 × ℝ) (j : Fin 5) : finAxisProj z j = if j = 4 then 0 else z.1 j

theorem CIV.norm_finAxisProj_apply_le (z : CKN.Vec 5 × ℝ) : ‖finAxisProj z‖ ≤ ‖z‖

theorem CIV.norm_finAxisProj_le : ‖finAxisProj‖ ≤ 1

def CIV.finAxisBump : ContDiffBump 0

The bump of the cutoff: 1 on the closed unit ball, 0 outside the open ball of radius 2.

Equations

• CIV.finAxisBump = { rIn := 1, rOut := 2, rIn_pos := CIV.finAxisBump._proof_2, rIn_lt_rOut := CIV.finAxisBump._proof_3 }

noncomputable def CIV.finAxisCutoff (ε : ℝ) (z : CKN.Vec 5 × ℝ) : ℝ

The cutoff b(X / ε) at scale ε near the axis of the lifted variables.

Equations

• CIV.finAxisCutoff ε z = ↑CIV.finAxisBump ((ε⁻¹ • CIV.finAxisProj) z)

theorem CIV.finAxisCutoff_eq_comp (ε : ℝ) : finAxisCutoff ε = ↑finAxisBump ∘ ⇑(ε⁻¹ • finAxisProj)

theorem CIV.contDiff_finAxisCutoff (ε : ℝ) : ContDiff ℝ (↑⊤) (finAxisCutoff ε)

theorem CIV.finAxisCutoff_nonneg (ε : ℝ) (z : CKN.Vec 5 × ℝ) : 0 ≤ finAxisCutoff ε z

theorem CIV.finAxisCutoff_le_one (ε : ℝ) (z : CKN.Vec 5 × ℝ) : finAxisCutoff ε z ≤ 1

theorem CIV.finAxisCutoff_eq_one {ε : ℝ} {z : CKN.Vec 5 × ℝ} (hz : ‖(ε⁻¹ • finAxisProj) z‖ ≤ 1) : finAxisCutoff ε z = 1

The cutoff is 1 where the rescaled radial part has norm at most one.

theorem CIV.finAxisCutoff_eq_zero {ε : ℝ} {z : CKN.Vec 5 × ℝ} (hz : 2 ≤ ‖(ε⁻¹ • finAxisProj) z‖) : finAxisCutoff ε z = 0

The cutoff vanishes where the rescaled radial part has norm at least two.

theorem CIV.exists_norm_iteratedFDeriv_finAxisBump_le : ∃ (C : ℝ), 0 ≤ C ∧ ∀ j ≤ 2, ∀ (y : CKN.Vec 5), ‖iteratedFDeriv ℝ j (↑finAxisBump) y‖ ≤ C

Derivative bounds for the fixed bump.

theorem CIV.norm_iteratedFDeriv_finAxisCutoff_le {C : ℝ} (hC : ∀ j ≤ 2, ∀ (y : CKN.Vec 5), ‖iteratedFDeriv ℝ j (↑finAxisBump) y‖ ≤ C) {ε : ℝ} (hε : 0 < ε) {j : ℕ} (hj : j ≤ 2) (z : CKN.Vec 5 × ℝ) : ‖iteratedFDeriv ℝ j (finAxisCutoff ε) z‖ ≤ C * ε⁻¹ ^ j

The j-th derivative of the cutoff at scale ε is O(ε^{-j}).

theorem CIV.le_zoomLiftRadius_of_one_le_norm {ε : ℝ} (hε : 0 < ε) {z : CKN.Vec 5 × ℝ} (hz : 1 ≤ ‖(ε⁻¹ • finAxisProj) z‖) : ε ≤ zoomLiftRadius z.1

Where the cutoff is not identically one nearby, some radial coordinate has size at least ε, so the lifted radius is at least ε.

theorem CIV.abs_apply_le_of_norm_le_two {ε : ℝ} (hε : 0 < ε) {z : CKN.Vec 5 × ℝ} (hz : ‖(ε⁻¹ • finAxisProj) z‖ ≤ 2) {j : Fin 5} (hj : j ≠ 4) : |z.1 j| ≤ 2 * ε

Where the rescaled radial part has norm at most two, every radial coordinate is at most 2ε.

The residual integrand

theorem CIV.abs_residualIntegrand_le {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ 2 ψ) (z : CKN.Vec 5 × ℝ) (v : CKN.Vec 5) (d : ℝ) : |-timeDeriv 5 ψ z - gradPair 5 ψ z v - d * ψ z - partialLaplacian 5 4 ψ z| ≤ (1 + ‖v‖) * ‖iteratedFDeriv ℝ 1 ψ z‖ + |d| * ‖iteratedFDeriv ℝ 0 ψ z‖ + 4 * ‖iteratedFDeriv ℝ 2 ψ z‖

The integrand -∂_τ ψ - v · ∇ψ - d ψ - Δ_X ψ of the residual of eq:aniso:zoom:finite:limit, bounded by the first two derivatives of ψ.

theorem CIV.residualIntegrand_add {ψa ψb : CKN.Vec 5 × ℝ → ℝ} (ha : ContDiff ℝ 2 ψa) (hb : ContDiff ℝ 2 ψb) (z : CKN.Vec 5 × ℝ) (v : CKN.Vec 5) (d : ℝ) : -timeDeriv 5 (fun (y : CKN.Vec 5 × ℝ) => ψa y + ψb y) z - gradPair 5 (fun (y : CKN.Vec 5 × ℝ) => ψa y + ψb y) z v - d * (ψa z + ψb z) - partialLaplacian 5 4 (fun (y : CKN.Vec 5 × ℝ) => ψa y + ψb y) z = -timeDeriv 5 ψa z - gradPair 5 ψa z v - d * ψa z - partialLaplacian 5 4 ψa z + (-timeDeriv 5 ψb z - gradPair 5 ψb z v - d * ψb z - partialLaplacian 5 4 ψb z)

The residual integrand is additive in the test function.

theorem CIV.norm_iteratedFDeriv_mul_le_of_forall_le {φ χ : CKN.Vec 5 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hχ : ContDiff ℝ (↑⊤) χ) {z : CKN.Vec 5 × ℝ} {A B : ℝ} (hA : ∀ j ≤ 2, ‖iteratedFDeriv ℝ j φ z‖ ≤ A) (hB : ∀ j ≤ 2, ‖iteratedFDeriv ℝ j χ z‖ ≤ B) {j : ℕ} (hj : j ≤ 2) : ‖iteratedFDeriv ℝ j (fun (y : CKN.Vec 5 × ℝ) => φ y * χ y) z‖ ≤ 4 * (A * B)

Derivatives of a product up to order two, from derivative bounds on the factors.

theorem CIV.exists_norm_iteratedFDeriv_le_of_hasCompactSupport {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ j ≤ 2, ∀ (z : CKN.Vec 5 × ℝ), ‖iteratedFDeriv ℝ j ψ z‖ ≤ A

Every derivative of order at most two of a compactly supported smooth function is bounded.

theorem CIV.residualIntegrand_eq_zero_of_notMem {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ 2 ψ) {z : CKN.Vec 5 × ℝ} (hz : z ∉ tsupport ψ) (v : CKN.Vec 5) (d : ℝ) : -timeDeriv 5 ψ z - gradPair 5 ψ z v - d * ψ z - partialLaplacian 5 4 ψ z = 0

The residual integrand vanishes off the support of the test function.

theorem CIV.integrable_mul_residualIntegrand {K : Set (CKN.Vec 5 × ℝ)} (hK : IsCompact K) {q d : CKN.Vec 5 × ℝ → ℝ} {b : CKN.Vec 5 × ℝ → CKN.Vec 5} {M : ℝ} (hq : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.restrict K)) (hbm : MeasureTheory.AEStronglyMeasurable b (MeasureTheory.volume.restrict K)) (hd : MeasureTheory.AEStronglyMeasurable d (MeasureTheory.volume.restrict K)) (hbd : ∀ z ∈ K, |q z| ≤ M ∧ ‖b z‖ ≤ M ∧ |d z| ≤ M) {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψK : tsupport ψ ⊆ K) : MeasureTheory.Integrable (fun (z : CKN.Vec 5 × ℝ) => q z * (-timeDeriv 5 ψ z - gradPair 5 ψ z (b z) - d z * ψ z - partialLaplacian 5 4 ψ z)) MeasureTheory.volume

Integrability of the pairing of a locally bounded scalar with the residual integrand of a test function.