OddReflectionSobolev

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

The Sobolev atom of the partial odd reflection

a smooth compactly supported function that vanishes on the reflection hyperplane {yᵢ = a} restricts to an H¹₀ function of the half it cuts out.

This is what turns the odd fold φ - φ ∘ r of a test function φ — the antisymmetric analogue of CoarseGraining's foldedCoordFaceTest — into an admissible H¹₀ competitor on the window side of a met face, which is how the odd extension inherits weak harmonicity.

The route

Let H = U ∩ {y : 0 < σ(a - yᵢ)} be the half (σ = ±1 selects the side). Cut off with the smooth profile

  χₙ(y) = θ( σ(a - yᵢ)(n+1) - 1 ) ,     θ = Real.smoothTransition ,

so that χₙ = 0 where σ(a - yᵢ) ≤ 1/(n+1) and χₙ = 1 where σ(a - yᵢ) ≥ 2/(n+1). Then χₙ·ψ is smooth and compactly supported inside H — literally an approximating sequence for H¹₀(H) — and the two error terms

  (1 - χₙ)·ψ ,   (1 - χₙ)·∂ⱼψ ,   ψ·∂ᵢχₙ

all vanish outside the strip Sₙ = H ∩ {σ(a - yᵢ)(n+1) < 2} and are bounded there by one n-independent constant: the mean value theorem gives |ψ(y)| ≤ L·|yᵢ - a| (because ψ vanishes on the face), while |∂ᵢχₙ| ≤ derivBound·(n+1), and on the support of ∂ᵢχₙ one has σ(a - yᵢ)(n+1) < 2, so the product is at most 2·L·derivBound. Since |Sₙ| → 0 (the sets decrease to the empty set inside the bounded U), all three tend to 0 in L²(H), and memH10_of_tendsto_H1 closes the argument.

What is not done here

Nothing about the odd extension itself: no gluing, no change of variables, no harmonicity.

References

• CoarseGraining Homogenization.Sobolev.Truncation.H10Limit (memH10_of_tendsto_H1), Homogenization.Sobolev.Foundations.Cutoff.Profile (smoothTransitionProfile, derivBound), Homogenization.Sobolev.H1.BasicLemmas (H1Function.ofContDiff, memH10_of_contDiff).

1. The half cut out by a coordinate hyperplane

def Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) : Set (HCPolySupport.Vec d)

The part of U strictly on the σ-side of the hyperplane {yᵢ = a}. Taking σ = 1 gives U ∩ {yᵢ < a}, taking σ = -1 gives U ∩ {a < yᵢ}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf U i a σ = U ∩ {y : HCPolySupport.Vec d | 0 < σ * (a - y i)}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf_subset {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) : faceHalf U i a σ ⊆ U

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_faceHalf_iff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {i : Fin d} {a σ : ℝ} {y : HCPolySupport.Vec d} : y ∈ faceHalf U i a σ ↔ y ∈ U ∧ 0 < σ * (a - y i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (i : Fin d) (a σ : ℝ) : IsOpen (faceHalf U i a σ)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.convex_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : Convex ℝ U) (i : Fin d) (a σ : ℝ) : Convex ℝ (faceHalf U i a σ)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isBoundedDomain_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsBoundedDomain U) (i : Fin d) (a σ : ℝ) : HCPolySupport.IsBoundedDomain (faceHalf U i a σ)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpenBoundedConvexDomain_faceHalf {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (i : Fin d) (a σ : ℝ) : HCPolySupport.IsOpenBoundedConvexDomain (faceHalf U i a σ)

2. The gap to the face, and the Lipschitz bound of a vanishing test

3. The interface cutoff

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff {d : ℕ} (i : Fin d) (a σ : ℝ) (n : ℕ) : HCPolySupport.Vec d → ℝ

The n-th interface cutoff: θ(σ(a - yᵢ)(n+1) - 1), vanishing within distance 1/(n+1) of the face and equal to 1 beyond 2/(n+1).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff i a σ n y = HCPolySupport.smoothTransitionProfile (σ * (a - y i) * (↑n + 1) - 1)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff_nonneg {d : ℕ} (i : Fin d) (a σ : ℝ) (n : ℕ) (y : HCPolySupport.Vec d) : 0 ≤ faceCutoff i a σ n y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff_le_one {d : ℕ} (i : Fin d) (a σ : ℝ) (n : ℕ) (y : HCPolySupport.Vec d) : faceCutoff i a σ n y ≤ 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff_eq_zero {d : ℕ} {i : Fin d} {a σ : ℝ} {n : ℕ} {y : HCPolySupport.Vec d} (h : σ * (a - y i) * (↑n + 1) ≤ 1) : faceCutoff i a σ n y = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceCutoff_eq_one {d : ℕ} {i : Fin d} {a σ : ℝ} {n : ℕ} {y : HCPolySupport.Vec d} (h : 2 ≤ σ * (a - y i) * (↑n + 1)) : faceCutoff i a σ n y = 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.contDiff_faceCutoff {d : ℕ} (i : Fin d) (a σ : ℝ) (n : ℕ) : ContDiff ℝ (↑⊤) (faceCutoff i a σ n)

4. The strip carrying the whole error

def Algsuperdiff.Section4.Provider.ExcessDecay.faceStrip {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) (n : ℕ) : Set (HCPolySupport.Vec d)

The vanishing strip: the part of the half within 2/(n+1) of the face.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.faceStrip U i a σ n = Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf U i a σ ∩ {y : HCPolySupport.Vec d | σ * (a - y i) * (↑n + 1) < 2}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceStrip_subset_faceHalf {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) (n : ℕ) : faceStrip U i a σ n ⊆ faceHalf U i a σ

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_faceStrip {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (i : Fin d) (a σ : ℝ) (n : ℕ) : IsOpen (faceStrip U i a σ n)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.antitone_faceStrip {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) : Antitone (faceStrip U i a σ)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.iInter_faceStrip {d : ℕ} (U : Set (HCPolySupport.Vec d)) (i : Fin d) (a σ : ℝ) : ⋂ (n : ℕ), faceStrip U i a σ n = ∅

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tendsto_volume_faceStrip {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (i : Fin d) (a σ : ℝ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.volume (faceStrip U i a σ n)) Filter.atTop (nhds 0)

5. An L² convergence criterion on a vanishing strip

6. The cutoff product and its differential

7. The atom

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memH10_faceHalf_of_contDiff_of_vanishing_on_face {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {i : Fin d} {a σ : ℝ} (hσ : |σ| = 1) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) (hψ0 : ∀ (y : HCPolySupport.Vec d), y i = a → ψ y = 0) : HCPolySupport.MemH10 (faceHalf U i a σ) ψ

: the Sobolev atom of the partial odd reflection.

A smooth compactly supported function on the domain U that vanishes on the hyperplane {yᵢ = a} restricts to an H¹₀ function of the half of U on either side of that hyperplane (σ = 1 the side yᵢ < a, σ = -1 the side a < yᵢ).

This is the one new Sobolev fact behind the draft's odd reflection: applied to the odd fold φ - φ ∘ r of a test function φ, it makes the fold an admissible H¹₀ competitor on the window side of a met face.