Weak integration by parts for tests with vanishing normal boundary jets
ProvedHunterPDE.Shared.HasWeakDeriv.integral_mul_normalJetVanishingLet H be an open coordinate half-space, and suppose f and its specified weak multi-derivative g are locally integrable with respect to the restriction of volume to H, including on compact sets meeting the boundary. If a globally smooth compactly supported test has all normal derivatives of orders strictly below the normal order of the specified multi-index equal to zero on the boundary hyperplane, then the weak integration-by-parts identity remains valid with this test. No conditions are imposed on other weak derivatives of f. When the normal order is zero, no boundary conditions are required. A proposed proof multiplies the test by interior normal cutoffs; Taylor vanishing controls every Leibniz error in a shrinking strip, and local integrability gives convergence. This general higher-order cutoff result is an Open proof obligation.
import Definitions.Def_HunterPDE_Shared_WeakDeriv open MeasureTheory HunterPDE.Shared set_option autoImplicit false
theorem HunterPDE.Shared.HasWeakDeriv.integral_mul_normalJetVanishing
{n : ℕ} (i : Fin n) (α : Fin n → ℕ)
(f g ψ : EuclideanSpace ℝ (Fin n) → ℝ)
(hf : LocallyIntegrable f (volume.restrict {x | 0 < x i}))
(hg : LocallyIntegrable g (volume.restrict {x | 0 < x i}))
(hd : HasWeakDeriv {x | 0 < x i} α f g)
(hψ : IsTestFunction Set.univ ψ)
(hb : ∀ r : ℕ, r < α i → ∀ x : EuclideanSpace ℝ (Fin n), x i = 0 →
iteratedPartial ψ (List.replicate r i) x = 0) :
(∫ x in {x : EuclideanSpace ℝ (Fin n) | 0 < x i}, g x * ψ x) =
(-1 : ℝ) ^ (∑ k, α k) *
∫ x in {x : EuclideanSpace ℝ (Fin n) | 0 < x i}, f x * multiDeriv ψ α x := by sorry