Test vector fields vanishing normally on a hyperplane

A test vector field whose normal component f ∘ χ vanishes on a hyperplane {f = a} has normal component O (|f - a|): StrongDual.exists_abs_apply_le_mul_abs_sub.

Given a hyperplane {f = c}, a test vector field φ extends its normal component off the hyperplane in a fixed direction w with f w = 1, by a smooth cutoff (StrongDual.exists_coe_eq_cutoff_normal_field); the extension is divergence-free above the hyperplane up to the cutoff (StrongDual.divergenceCLM_cutoff_normal_field). Two admissible test vector fields are interpolated across the hyperplane by the smooth transition (StrongDual.exists_interpolation_divergence), with an error term which is uniformly bounded when the normal component of their difference vanishes on the hyperplane (StrongDual.exists_abs_deriv_smoothTransition_mul_le_indicator).

theorem StrongDual.exists_abs_apply_le_mul_abs_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : StrongDual ℝ E) (a : ℝ) {Ω : TopologicalSpace.Opens E} {χ : TestFunction Ω E ⊤} (hχ : ∀ (x : E), f x = a → f (χ x) = 0) : ∃ (C : ℝ), ∀ (x : E), |f (χ x)| ≤ C * |f x - a|

A test vector field whose normal component f ∘ χ vanishes on the hyperplane {f = a} has normal component O (|f - a|).

theorem StrongDual.exists_coe_eq_cutoff_normal_field {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : StrongDual ℝ E) (c : ℝ) (w : E) (φ : TestFunction ⊤ E ⊤) (n : ℕ) : ∃ (ψ : TestFunction ⊤ E ⊤), ⇑ψ = fun (x : E) => ((f x - c + 1).smoothTransition * (1 - (f x - (c + ↑n)).smoothTransition) * f (φ (x - (f x - c) • w))) • w

The cutoff field x ↦ η (f x) · f (φ (x - (f x - c) • w)) • w used to extend the normal component of φ off the hyperplane {f = c} is a test vector field, where w is any vector and η is a smooth cutoff equal to one on [c, c + n].

theorem StrongDual.divergenceCLM_cutoff_normal_field {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : StrongDual ℝ E) (c : ℝ) {w : E} (hw : f w = 1) (φ : TestFunction ⊤ E ⊤) (n : ℕ) {ψ : TestFunction ⊤ E ⊤} (hψ : ⇑ψ = fun (x : E) => ((f x - c + 1).smoothTransition * (1 - (f x - (c + ↑n)).smoothTransition) * f (φ (x - (f x - c) • w))) • w) {x : E} (hx : c < f x) : (TestFunction.divergenceCLM ψ) x = -(deriv Real.smoothTransition (f x - (c + ↑n)) * f (φ (x - (f x - c) • w)))

Above the hyperplane {f = c}, the divergence of the cutoff field of StrongDual.exists_coe_eq_cutoff_normal_field only sees the upper cutoff.

theorem StrongDual.exists_abs_deriv_smoothTransition_mul_le_indicator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : StrongDual ℝ E) (a : ℝ) {Ω : TopologicalSpace.Opens E} {χ : TestFunction Ω E ⊤} (hχ : ∀ (x : E), f x = a → f (χ x) = 0) : ∃ (K : ℝ), ∀ (n : ℕ) (x : E), |deriv Real.smoothTransition ((↑n + 1) * (f x - a)) * ((↑n + 1) * f (χ x))| ≤ (tsupport ⇑χ).indicator (fun (x : E) => K) x

The error term ψ₀' ((n + 1) (f - a)) (n + 1) f (χ) of the interpolation of two test vector fields is dominated, uniformly in n, by a constant on the support of χ, when the normal component of χ vanishes on the hyperplane {f = a}.

theorem StrongDual.exists_interpolation_divergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : StrongDual ℝ E) (a : ℝ) {Ω : TopologicalSpace.Opens E} {φ ψ : TestFunction Ω E ⊤} (hφ : ∀ (x : E), ‖φ x‖ ≤ 1) (hψ : ∀ (x : E), ‖ψ x‖ ≤ 1) : ∃ (Φ : ℕ → TestFunction Ω E ⊤), (∀ (n : ℕ) (x : E), ‖(Φ n) x‖ ≤ 1) ∧ ∀ (n : ℕ) (x : E), (TestFunction.divergenceCLM (Φ n)) x = (TestFunction.divergenceCLM φ) x + ((↑n + 1) * (f x - a)).smoothTransition * (TestFunction.divergenceCLM (ψ - φ)) x + deriv Real.smoothTransition ((↑n + 1) * (f x - a)) * ((↑n + 1) * f ((ψ - φ) x))

Interpolating two admissible test vector fields φ and ψ across the hyperplane {f = a} by Φₙ = φ + σₙ (ψ - φ), where σₙ = ψ₀ ((n + 1) (f - a)) for the smooth transition ψ₀, gives admissible test vector fields, with divergence div φ + σₙ div (ψ - φ) + σₙ' f (ψ - φ).