Internal support lemmas for the interior estimate

Shared scaffolding for the modules under EllipticPdes.Regularity.Interior. These declarations are internal: they are exposed only because Lean's private modifier is file-scoped and the interior estimate spans several modules. Each lemma here is stated and proved once but consumed in more than one of them, so no single module can keep it private.

Consumers should use interior_H2_estimate and its siblings from EllipticPdes.Regularity.Interior.

theorem EllipticPdes.Regularity.mulTest_ae_eq_zero_off_tsupport {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (g : Sobolev.L2D Ω) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, x ∉ tsupport η → ↑↑((mulTest hη) g) x = 0

A cutoff-multiplied class vanishes a.e. off the topological support of the cutoff.

theorem EllipticPdes.Regularity.extendL2_supp_of_ae_restrict {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) {S : Set (EuclideanSpace ℝ (Fin d))} (hg : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, x ∉ S → ↑↑g x = 0) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ↑↑((extendL2 hΩm) g) x ≠ 0 → x ∈ S

If a class g vanishes a.e. (on Ω) off a set S, then its extension by zero to the whole space is a.e. supported in S.

theorem EllipticPdes.Regularity.norm_restrictL2_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (w : ↥(MeasureTheory.EucL2 d)) : ‖restrictL2 w‖ ≤ ‖w‖

Restriction to Ω is non-expansive on L²: ‖restrictL2 w‖ ≤ ‖w‖.

theorem EllipticPdes.Regularity.single_le_sum_fin {m : ℕ} (g : Fin m → ℝ) (hg : ∀ (i : Fin m), 0 ≤ g i) (k : Fin m) : g k ≤ ∑ i : Fin m, g i

Abstract single-term ≤ sum over Fin d for a nonnegative real family, isolated so its application only beta-reduces (avoiding a Finset.single_le_sum isDefEq loop on L² norm summands).