Coarse-graining support: Support.Sobolev.CubeEmbedding.Extension

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Even-fold extension of an H¹(box) function

Given u ∈ H¹(Box lo hi), its even-fold extension Eu (x) = u (Fold lo hi x) (with the signed folded gradient) is an H¹(Box3 lo hi) function whose L² norms on the tripled box are controlled by (3^d)^{1/2} times the L² norms of u on the base box, and which agrees with u a.e. on the base box.

The construction feeds the globally smooth convexApproxSmoothH1 approximants of u, cut off to compact support, through the per-approximant fold weak-gradient identity (hasWeakPartialDerivOn_univ_foldComp) and closes under L² limits (HasWeakGradientOn.of_tendsto_eLpNorm_two); the norm transport is supplied by FoldNorm.

Geometry of the base box

theorem HCPolySupport.isOpen_Box {d : ℕ} (lo hi : Vec d) : IsOpen (Box lo hi)

theorem HCPolySupport.isOpenBoundedConvexDomain_Box {d : ℕ} (lo hi : Vec d) : IsOpenBoundedConvexDomain (Box lo hi)

theorem HCPolySupport.Box3_eq_Box {d : ℕ} (lo hi : Vec d) : Box3 lo hi = Box (fun (k : Fin d) => 2 * lo k - hi k) fun (k : Fin d) => 2 * hi k - lo k

The tripled box is the base box for the reflected corners.

theorem HCPolySupport.exists_ball_subset_Box {d : ℕ} (lo hi : Vec d) (hlt : ∀ (k : Fin d), lo k < hi k) (hd : 0 < d) : ∃ (x0 : Vec d) (r : ℝ), 0 < r ∧ Metric.closedBall x0 r ⊆ Box lo hi

A concrete closed ball inside a nonempty base box.

eLpNorm convergence of the smooth approximants

theorem HCPolySupport.tendsto_eLpNorm_convexApproxSmoothH1 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {x0 : Vec d} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x0 r ⊆ U) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (H1Function.convexApproxSmoothH1 hU u x0 hr n).toFun x - u.toFun x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

Convergence in L²(U) of the convexApproxSmoothH1 approximants, in the eLpNorm form the closure lemma consumes.

theorem HCPolySupport.tendsto_eLpNorm_grad_convexApproxSmoothH1 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {x0 : Vec d} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x0 r ⊆ U) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (H1Function.convexApproxSmoothH1 hU u x0 hr n).grad x i - u.grad x i) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

Convergence in L²(U) of the coordinate gradients of the approximants.

The fold extension

structure HCPolySupport.FoldExtension {d : ℕ} (lo hi : Vec d) (u : H1Function (Box lo hi)) : Type

The fold-extension data bundle.

• Eu : H1Function (Box3 lo hi)

  The extended H¹ function on the tripled box.

• toFun_ae : self.Eu.toFun =ᵐ[MeasureTheory.volume.restrict (Box lo hi)] u.toFun

  The extension agrees with u a.e. on the base box.

• grad_ae (i : Fin d) : (fun (x : Vec d) => self.Eu.grad x i) =ᵐ[MeasureTheory.volume.restrict (Box lo hi)] fun (x : Vec d) => u.grad x i

  The extension's gradient agrees with u's a.e. on the base box.

• eLpNorm_le : MeasureTheory.eLpNorm self.Eu.toFun 2 (MeasureTheory.volume.restrict (Box3 lo hi)) ≤ (3 ^ d) ^ (1 / 2) * MeasureTheory.eLpNorm u.toFun 2 (MeasureTheory.volume.restrict (Box lo hi))

  L² control of the extension by the constant (3^d)^{1/2}.

• grad_eLpNorm_le (i : Fin d) : MeasureTheory.eLpNorm (fun (x : Vec d) => self.Eu.grad x i) 2 (MeasureTheory.volume.restrict (Box3 lo hi)) ≤ (3 ^ d) ^ (1 / 2) * MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) 2 (MeasureTheory.volume.restrict (Box lo hi))

  L² control of the extension's coordinate gradients.

theorem HCPolySupport.Cd_ne_top {d : ℕ} : (3 ^ d) ^ (1 / 2) ≠ ⊤

Cd = (3^d)^{1/2} is finite.

theorem HCPolySupport.measurable_foldSign_comp {d : ℕ} (lo hi : Vec d) (i : Fin d) : Measurable fun (x : Vec d) => foldSign (lo i) (hi i) (x i)

theorem HCPolySupport.norm_foldSign_le_one (lo hi t : ℝ) : ‖foldSign lo hi t‖ ≤ 1