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

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

The even-periodic fold onto a box

The coordinatewise even fold of ℝ onto the interval [lo, hi] with margin equal to the side length: identity on [lo, hi], reflected across lo below and across hi above. Applied coordinatewise it gives Fold : Vec d → Vec d, and the extension of a function v is v ∘ Fold. There are only two kinks per coordinate; the fold is 1-Lipschitz and equals the identity on the closed box.

noncomputable def HCPolySupport.foldR (lo hi t : ℝ) : ℝ

Scalar even fold of ℝ onto [lo, hi]: reflected across lo below, across hi above, identity in between.

Equations

• HCPolySupport.foldR lo hi t = if t < lo then 2 * lo - t else if hi < t then 2 * hi - t else t

noncomputable def HCPolySupport.foldSign (lo hi t : ℝ) : ℝ

The (right) derivative sign of foldR: -1 on the reflected pieces, +1 in the interior.

Equations

• HCPolySupport.foldSign lo hi t = if t < lo then -1 else if hi < t then -1 else 1

noncomputable def HCPolySupport.Fold {d : ℕ} (lo hi x : Vec d) : Vec d

The coordinatewise fold onto the box [lo, hi].

Equations

• HCPolySupport.Fold lo hi x j = HCPolySupport.foldR (lo j) (hi j) (x j)

@[simp]

theorem HCPolySupport.foldR_of_mem {lo hi t : ℝ} (h1 : lo ≤ t) (h2 : t ≤ hi) : foldR lo hi t = t

theorem HCPolySupport.continuous_foldR (lo hi : ℝ) (h : lo ≤ hi) : Continuous (foldR lo hi)

theorem HCPolySupport.continuous_Fold {d : ℕ} (lo hi : Vec d) (hlohi : ∀ (j : Fin d), lo j ≤ hi j) : Continuous (Fold lo hi)

theorem HCPolySupport.Fold_of_mem {d : ℕ} {lo hi x : Vec d} (h : ∀ (j : Fin d), lo j ≤ x j ∧ x j ≤ hi j) : Fold lo hi x = x

The fold is the identity on the closed box.

theorem HCPolySupport.Fold_insertNth {n : ℕ} (lo hi : Vec (n + 1)) (j : Fin (n + 1)) (t : ℝ) (z : Vec n) : Fold lo hi (j.insertNth t z) = j.insertNth (foldR (lo j) (hi j) t) fun (m : Fin n) => foldR (lo (j.succAbove m)) (hi (j.succAbove m)) (z m)

Expansion of the fold along an insertion line: only the j-coordinate varies, through foldR (lo j) (hi j) t; the tangential coordinates are frozen.