OddReflectionGlue

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

The H¹ gluing of the odd reflection across one face

Three steps, each proved here:

1. L² graph closure (hasWeakGradientOn_of_tendsto_lp): the weak-gradient graph is closed under L² convergence of the function together with all of its gradient coordinates.
2. Zero extension (hasWeakGradientOn_univ_zeroExtend): the literal zero extension of an H¹₀(V) function has the zero-extended gradient as a global weak gradient. This is where the H¹₀ approximants earn their keep: they are already supported in V, so integration by parts against a test function supported anywhere in ℝᵈ is legitimate for each approximant, and the limit is taken in L².
3. Reflection transport (hasWeakGradientOn_univ_comp_coordFaceReflection): pre-composition with the face reflection r transports the weak gradient by the reflected gradient coordReflectionLinear i ∘ G ∘ r; the change of variables is measurePreserving_coordFaceReflection and the sign is the one-face chain rule euclideanCoordDeriv_comp_coordFaceReflection.

Together, the odd extension W - W ∘ r of the zero extension W of an H¹₀(V)-function of the half is H¹ on ℝᵈ (hasWeakGradientOn_univ_oddFaceExtend), and it is the expected pointwise odd extension: it is W on the half and -W ∘ r on the reflected half (oddFaceExtend_zeroExtend_of_mem, oddFaceExtend_zeroExtend_of_notMem).

What is not done here

The multi-face assembly — that the iterated oddExtend of OddReflectionMap is H¹ on the whole partially reflected window — is not proved here; only the single-face gluing is, which is the step the interface argument actually needs (the met faces are pairwise orthogonal, not_meetsLowerFace_of_meetsUpperFace, so a neighbourhood of any interface point meets exactly one of them).

References

• CoarseGraining Homogenization.Sobolev.W1p.WeakGradientClosure, Homogenization.Sobolev.W1p.ZeroExtensionGraph (route source; no oleans).
• CoarseGraining Homogenization.Sobolev.Foundations.CubeReflection.Reflections (measurePreserving_coordFaceReflection, coordFaceReflection_involutive), .CubeReflection.Derivatives (euclideanCoordDeriv_comp_coordFaceReflection), .CubeReflection.Homeomorphism (coordFaceReflectionHomeomorph).

1. L² closure of the weak-gradient graph

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakPartialDerivOn_of_tendsto_lp {d : ℕ} {U : Set (HCPolySupport.Vec d)} (p : HCPolySupport.FiniteLpExponent) {i : Fin d} {u gi : HCPolySupport.Vec d → ℝ} {u_n g_n : ℕ → HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u p.exponent (MeasureTheory.volume.restrict U)) (hgi : MeasureTheory.MemLp gi p.exponent (MeasureTheory.volume.restrict U)) (hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) p.exponent (MeasureTheory.volume.restrict U)) (hg_n : ∀ (n : ℕ), MeasureTheory.MemLp (g_n n) p.exponent (MeasureTheory.volume.restrict U)) (hweak : ∀ (n : ℕ), HCPolySupport.HasWeakPartialDerivOn U i (u_n n) (g_n n)) (htend_u : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u_n n x - u x) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) (htend_g : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => g_n n x - gi x) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : HCPolySupport.HasWeakPartialDerivOn U i u gi

Graph closure, one coordinate. Re-derivation of CoarseGraining's HasWeakPartialDerivOn.of_tendsto_eLpNorm_finiteLp (no olean upstream).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_of_tendsto_lp {d : ℕ} {U : Set (HCPolySupport.Vec d)} (p : HCPolySupport.FiniteLpExponent) {u : HCPolySupport.Vec d → ℝ} {Du : HCPolySupport.Vec d → HCPolySupport.Vec d} {u_n : ℕ → HCPolySupport.Vec d → ℝ} {Du_n : ℕ → HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u p.exponent (MeasureTheory.volume.restrict U)) (hDu : HCPolySupport.GradMemLpOn U p.exponent Du) (hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) p.exponent (MeasureTheory.volume.restrict U)) (hDu_n : ∀ (n : ℕ), HCPolySupport.GradMemLpOn U p.exponent (Du_n n)) (hweak : ∀ (n : ℕ), HCPolySupport.HasWeakGradientOn U (u_n n) (Du_n n)) (htend_u : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u_n n x - u x) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) (htend_Du : ∀ (i : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => Du_n n x i - Du x i) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : HCPolySupport.HasWeakGradientOn U u Du

Graph closure. Re-derivation of CoarseGraining's HasWeakGradientOn.of_tendsto_eLpNorm_finiteLp (no olean upstream).

2. Zero extension of an H¹₀ function

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtend {d : ℕ} (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d → ℝ

The literal zero extension of a scalar off V.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtend V u = V.indicator u

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendGrad {d : ℕ} (V : Set (HCPolySupport.Vec d)) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The literal zero extension of a gradient field off V.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendGrad V G = V.indicator G

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtend_of_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (u : HCPolySupport.Vec d → ℝ) {y : HCPolySupport.Vec d} (hy : y ∈ V) : zeroExtend V u y = u y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtend_of_notMem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (u : HCPolySupport.Vec d → ℝ) {y : HCPolySupport.Vec d} (hy : y ∉ V) : zeroExtend V u y = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendGrad_of_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (G : HCPolySupport.Vec d → HCPolySupport.Vec d) {y : HCPolySupport.Vec d} (hy : y ∈ V) : zeroExtendGrad V G y = G y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendGrad_of_notMem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (G : HCPolySupport.Vec d → HCPolySupport.Vec d) {y : HCPolySupport.Vec d} (hy : y ∉ V) : zeroExtendGrad V G y = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendGrad_apply_coord {d : ℕ} (V : Set (HCPolySupport.Vec d)) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) : (fun (y : HCPolySupport.Vec d) => zeroExtendGrad V G y i) = V.indicator fun (y : HCPolySupport.Vec d) => G y i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memL2_zeroExtend {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) : MeasureTheory.MemLp (zeroExtend V u.toFun) 2 MeasureTheory.volume

theorem Algsuperdiff.Section4.Provider.ExcessDecay.gradMemL2_zeroExtendGrad {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) : HCPolySupport.GradMemLpOn Set.univ 2 (zeroExtendGrad V u.grad)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_univ_zeroExtend {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) : HCPolySupport.HasWeakGradientOn Set.univ (zeroExtend V u.toFun) (zeroExtendGrad V u.grad)

, step 2: the zero extension is a global weak-gradient graph. Re-derivation of CoarseGraining's H10Function.hasWeakGradientOn_univ_zeroExtension (no olean upstream).

3. Reflection transport of a global weak gradient

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordReflectionLinear_apply_coord {d : ℕ} (i : Fin d) (v : HCPolySupport.Vec d) (k : Fin d) : (HCPolySupport.coordReflectionLinear i) v k = (if k = i then -1 else 1) * v k

4. The one-face odd extension is H¹ across the interface

def Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtend {d : ℕ} (a : ℝ) (i : Fin d) (w : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d → ℝ

The odd extension of a scalar across the face {yᵢ = a}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtend a i w y = w y - w (HCPolySupport.coordFaceReflection a i y)

def Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtendGrad {d : ℕ} (a : ℝ) (i : Fin d) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The gradient field of the odd extension.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtendGrad a i G y = G y - (HCPolySupport.coordReflectionLinear i) (G (HCPolySupport.coordFaceReflection a i y))

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtend_comp_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) (w : HCPolySupport.Vec d → ℝ) (y : HCPolySupport.Vec d) : oddFaceExtend a i w (HCPolySupport.coordFaceReflection a i y) = -oddFaceExtend a i w y

The odd extension is odd, as its name says.

5. The pointwise shape of the one-face odd extension

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordFaceReflection_notMem_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} {i : Fin d} {a σ : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ faceHalf U i a σ) : HCPolySupport.coordFaceReflection a i y ∉ faceHalf U i a σ

The reflection of a point of the σ-half proves outside it.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtend_zeroExtend_of_mem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (u : HCPolySupport.Vec d → ℝ) (a : ℝ) (i : Fin d) {y : HCPolySupport.Vec d} (hy : y ∈ V) (hry : HCPolySupport.coordFaceReflection a i y ∉ V) : oddFaceExtend a i (zeroExtend V u) y = u y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddFaceExtend_zeroExtend_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.Vec d → ℝ) {i : Fin d} {a σ : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ faceHalf U i a σ) : oddFaceExtend a i (zeroExtend (faceHalf U i a σ) u) y = u y

On the half itself the odd extension of the zero extension is the original function.