One null set for every second-order test pairing

A second-order distributional identity on time slices is first obtained one test function at a time, and the exceptional set of times then depends on the test function. Testing instead against the countable family of mollifier bumps centred at the points of a countable dense set produces a single null set, and the mollifier-bump upgrade recovers every smooth compactly supported test function from that countable family. This is the second-order counterpart of the divergence-form and multiplication-form upgrades used for the slice identities.

theorem CKN.slice_second_pairing_zero_of_mollifier_family {Q : Set Foundation.Parabolic.Vec3} (hQ : Dense Q) {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.LocallyIntegrable (G i j) MeasureTheory.volume) (hzero : ∀ y ∈ Q, ∀ (n : ℕ), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond (fun (z : Foundation.Parabolic.Vec3) => mollifier (sliceRadius n) ⋯ (z - y)) i j x = 0) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond ψ i j x = 0

The second-order instance of the mollifier-bump family upgrade. If the second-order pairing of a locally integrable matrix field G vanishes against the mixed second derivatives of every mollifier bump centred at a point of a dense set, then it vanishes against the mixed second derivatives of every smooth compactly supported test function.

theorem CKN.ae_slice_second_pairing_zero_of_forall_test {I : Set ℝ} {G : ℝ → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i j : Fin 3), MeasureTheory.LocallyIntegrable (G s i j) MeasureTheory.volume) (hzero : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G s i j x * mixedSecond ψ i j x = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G s i j x * mixedSecond ψ i j x = 0

One null set for every test function, second-order form. If for each smooth compactly supported ψ the second-order slice pairing vanishes for almost every time, and almost every slice of the matrix field is locally integrable, then for almost every time the pairing vanishes for every such ψ.