Two auxiliary steps for slicing distributional identities

The passage from a countable family of mollifier bumps to every test function uses two ingredients that are independent of the differential operator at hand.

• eq_zero_of_dense_of_continuousAt: a function that is continuous on an open set and vanishes on a dense subset vanishes on the whole open set.
• integral_mul_integral_translate_swap: Fubini for the pairing of a compactly supported continuous function with the translation average of an integrable function against a compactly supported continuous kernel.

theorem CKN.eq_zero_of_dense_of_continuousAt {X : Type u_1} [TopologicalSpace X] {D : X → ℝ} {U S : Set X} (hS : Dense S) (hU : IsOpen U) (hcont : ∀ y ∈ U, ContinuousAt D y) (hzero : ∀ y ∈ U ∩ S, D y = 0) (y : X) : y ∈ U → D y = 0

A real function that is continuous at every point of an open set U and vanishes on U ∩ S for a dense set S vanishes on all of U.

theorem CKN.integrable_uncurry_mul_translate {d : ℕ} {ψ G k : Vec d → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hk : Continuous k) (hkc : HasCompactSupport k) : MeasureTheory.Integrable (Function.uncurry fun (y x : Vec d) => ψ y * (G x * k (x - y))) (MeasureTheory.volume.prod MeasureTheory.volume)

The double integrand of the pairing of ψ with the translation averages of G against k is integrable for the product measure.

theorem CKN.integrable_mul_integral_translate {d : ℕ} {ψ G k : Vec d → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hk : Continuous k) (hkc : HasCompactSupport k) : MeasureTheory.Integrable (fun (y : Vec d) => ψ y * ∫ (x : Vec d), G x * k (x - y)) MeasureTheory.volume

The pairing of a compactly supported continuous function ψ with the translation averages of an integrable function G against a compactly supported continuous kernel k is itself integrable.

theorem CKN.integral_mul_integral_translate_swap {d : ℕ} {ψ G k : Vec d → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hk : Continuous k) (hkc : HasCompactSupport k) : ∫ (y : Vec d), ψ y * ∫ (x : Vec d), G x * k (x - y) = ∫ (x : Vec d), G x * ∫ (y : Vec d), ψ y * k (x - y)

Exchanging the order of integration in the pairing of a compactly supported continuous function ψ with the translation averages of an integrable function G against a compactly supported continuous kernel k.