OneStepOddPackagingCore

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The H¹ packaging of the odd extension: the core atoms

This module builds the three named ingredients that produce it from a face-only zero-trace hypothesis — the honest input identified in the one-met-face scope note: full H¹₀-membership of the competitor would force it to vanish.

• The interface eta-cutoff chain. The face-only zero trace is rendered by CoarseGraining's own LocalizedZeroTraceFunctionOn Ω V: every smooth cutoff supported in the localization window V turns the function into an H¹₀(Ω) member. With Ω the window half and V the reflected window, a cutoff supported in V vanishes near ∂V — hence near every part of ∂Ω except the interface hyperplane, which is interior to V. This is exactly "zero trace on the met face only", with no trace operator. setIntegral_mul_fderiv_of_localizedZeroTrace is the resulting integration by parts: ∫_Ω v ∂ⱼψ = -∫_Ω ∂ⱼv ψ for smooth ψ supported in V (not in Ω! — ψ may be nonzero on the interface). The chain: a smooth bump η ≡ 1 on a neighbourhood of tsupport ψ (exists_contDiff_eq_one_on_isCompact, the compact-set upgrade of exists_contDiff_eq_one_nhds); the H¹₀ member η·v; its global zero extension (OddReflectionGlue.hasWeakGradientOn_univ_zeroExtend); the global test identity; and the collapse back to Ω.

• The a.e.-congruence atom. The H¹₀ witness of η·v records some weak gradient; on the open region where η ≡ 1 it is a weak gradient of v itself, so by the a.e. uniqueness of weak derivatives on open sets (CoarseGraining's HasWeakPartialDerivOn.ae_eq) it agrees a.e. with v.grad there — and the test ψ is supported there. hasWeakPartialDerivOn_congr_left is the value congruence that makes the identification legitimate.

References

• CoarseGraining Homogenization/Sobolev/H1/LocalizedZeroTrace.lean (the predicate), Homogenization/Sobolev/W1p/ZeroExtensionGraph.lean (the zero extension).

1. A smooth bump identically one on a compact set

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_contDiff_eq_one_on_isCompact {d : ℕ} {K U : Set (HCPolySupport.Vec d)} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (η : HCPolySupport.Vec d → ℝ) (N : Set (HCPolySupport.Vec d)), ContDiff ℝ (↑⊤) η ∧ HasCompactSupport η ∧ tsupport η ⊆ U ∧ IsOpen N ∧ K ⊆ N ∧ ∀ y ∈ N, η y = 1

A smooth bump identically one on a neighbourhood of a compact set. The compact-set upgrade of exists_contDiff_eq_one_nhds, by the same product trick that drives exists_smooth_decomposition_of_open_cover: the defects 1 - g of finitely many pointwise bumps annihilate on a neighbourhood of K.

2. H¹₀ closure facts

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_mono_window {d : ℕ} {Ω V V' : Set (HCPolySupport.Vec d)} (hV' : V' ⊆ V) {f : HCPolySupport.Vec d → ℝ} (h : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V f) : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V' f

Shrinking the localization window weakens the localized zero-trace condition.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memH10_zeroExtend_of_subset {d : ℕ} {A B : Set (HCPolySupport.Vec d)} (hA : MeasurableSet A) (hB : IsOpen B) (hAB : A ⊆ B) {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemH10 A f) : HCPolySupport.MemH10 B (zeroExtend A f)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_comp_coordFaceReflection_of_symm {d : ℕ} {Ω : Set (HCPolySupport.Vec d)} (hΩ : MeasurableSet Ω) (a : ℝ) (i : Fin d) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ Ω ↔ y ∈ Ω) {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Ω w G) : HCPolySupport.HasWeakGradientOn Ω (fun (y : HCPolySupport.Vec d) => w (HCPolySupport.coordFaceReflection a i y)) fun (y : HCPolySupport.Vec d) => (HCPolySupport.coordReflectionLinear i) (G (HCPolySupport.coordFaceReflection a i y))

The restricted reflection transport. The weak gradient transports under pre-composition with the face reflection on any reflection-invariant measurable set — the Ω-restricted twin of OddReflectionGlue.hasWeakGradientOn_univ_comp_coordFaceReflection.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memH10_comp_coordFaceReflection {d : ℕ} {Ω : Set (HCPolySupport.Vec d)} (hΩ : MeasurableSet Ω) (a : ℝ) (i : Fin d) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ Ω ↔ y ∈ Ω) {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemH10 Ω f) : HCPolySupport.MemH10 Ω fun (y : HCPolySupport.Vec d) => f (HCPolySupport.coordFaceReflection a i y)

H¹₀ is closed under composition with a face reflection on a reflection-invariant measurable set.

3. The a.e.-congruence atom

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakPartialDerivOn_congr_left {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) {j : Fin d} {f f' g : HCPolySupport.Vec d → ℝ} (h : HCPolySupport.HasWeakPartialDerivOn W j f g) (hff' : ∀ y ∈ W, f y = f' y) : HCPolySupport.HasWeakPartialDerivOn W j f' g

The weak partial derivative predicate depends on the function only through its values on the window.

4. The interface eta-cutoff chain

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_mul_fderiv_of_localizedZeroTrace {d : ℕ} {Ω V : Set (HCPolySupport.Vec d)} (hΩ : IsOpen Ω) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict Ω)] (hV : IsOpen V) (v : HCPolySupport.H1Function Ω) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V v.toFun) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψV : tsupport ψ ⊆ V) (j : Fin d) : ∫ (y : HCPolySupport.Vec d) in Ω, v.toFun y * (fderiv ℝ ψ y) (HCPolySupport.basisVec j) = -∫ (y : HCPolySupport.Vec d) in Ω, v.grad y j * ψ y

Integration by parts against a test supported in the localization window. v ∈ H¹(Ω) has localized zero trace in V ⊇ the interface; then for every smooth compactly supported ψ with tsupport ψ ⊆ V,

∫_Ω v ∂ⱼψ = -∫_Ω (∇v)ⱼ ψ.

The test may be nonzero on the part of ∂Ω interior to V — that is exactly what the zero-trace hypothesis pays for.