DataApproximation

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

A countable subclass approximating every normalized forcing field uniformly

The normalized forcing fields of Section 5.1 are 1/2-Hölder on the open cube and unconstrained outside it, so they are not points of a metric space of their own. Dilating the closed cube towards its centre by a factor 1 - δ maps it into the open cube, so composing a forcing field with that dilation produces a field that is continuous on the closed cube, is again 1/2-Hölder with the same constant — the dilation is a contraction — and is uniformly close to the original on the cube, by the Hölder bound and the diameter of the cube.

Second countability of C(closedCubeAt y n, Vec d) then supplies a countable subclass of the dilated fields dense in the supremum distance, and hence a single countable family that approximates every normalized forcing field uniformly on the cube. This is the family the suprema of the localized quantities are realized on.

Main definitions

• shrinkTo y delta — the dilation of ℝ^d towards y by the factor 1 - delta.

Main results

• shrinkTo_mem_cubeSetAt, norm_sub_shrinkTo_le — the dilation maps the closed cube into the open cube and moves points by at most delta · 3^n / 2.
• exists_continuousMap_holder_close — one continuous field on the closed cube with the same Hölder constant and prescribed uniform closeness.
• exists_countable_holder_approx, exists_countable_normalizedForceAt_approx — the countable family.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. The dilation towards the centre

def Algsuperdiff.Section5.Support.shrinkTo {d : ℕ} (y : HCPolySupport.Vec d) (delta : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

The dilation of ℝ^d towards y by the factor 1 - delta.

Equations

• Algsuperdiff.Section5.Support.shrinkTo y delta x i = y i + (1 - delta) * (x i - y i)

theorem Algsuperdiff.Section5.Support.shrinkTo_apply {d : ℕ} (y : HCPolySupport.Vec d) (delta : ℝ) (x : HCPolySupport.Vec d) (i : Fin d) : shrinkTo y delta x i = y i + (1 - delta) * (x i - y i)

theorem Algsuperdiff.Section5.Support.continuous_shrinkTo {d : ℕ} (y : HCPolySupport.Vec d) (delta : ℝ) : Continuous (shrinkTo y delta)

theorem Algsuperdiff.Section5.Support.shrinkTo_sub {d : ℕ} (y : HCPolySupport.Vec d) (delta : ℝ) (x z : HCPolySupport.Vec d) : shrinkTo y delta x - shrinkTo y delta z = (1 - delta) • (x - z)

theorem Algsuperdiff.Section5.Support.shrinkTo_mem_cubeSetAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {delta : ℝ} (h0 : 0 < delta) (h1 : delta ≤ 1) {x : HCPolySupport.Vec d} (hx : x ∈ closedCubeAt y n) : shrinkTo y delta x ∈ cubeSetAt y n

The dilation maps the closed cube into the open cube.

theorem Algsuperdiff.Section5.Support.norm_sub_shrinkTo_le {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {delta : ℝ} (h0 : 0 ≤ delta) {x : HCPolySupport.Vec d} (hx : x ∈ closedCubeAt y n) : ‖x - shrinkTo y delta x‖ ≤ delta * (1 / 2 * 3 ^ n)

The dilation moves a point of the closed cube by at most delta · 3^n / 2.

2. The dilated field is a continuous field on the closed cube

theorem Algsuperdiff.Section5.Support.exists_extendVec_shrinkTo {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) {delta : ℝ} (h0 : 0 < delta) (h1 : delta ≤ 1) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : ContinuousOn g (cubeSetAt y n)) : ∃ (G : C(↑(closedCubeAt y n), HCPolySupport.Vec d)), ∀ x ∈ closedCubeAt y n, extendVec y n G x = g (shrinkTo y delta x)

3. One uniformly close field with the same Hölder constant

theorem Algsuperdiff.Section5.Support.exists_continuousMap_holder_close {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) {K : ℝ} (hK : 0 ≤ K) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) K g) {eta : ℝ} (heta : 0 < eta) : ∃ (G : C(↑(closedCubeAt y n), HCPolySupport.Vec d)), Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) K (extendVec y n G) ∧ ∀ x ∈ cubeSetAt y n, ‖g x - extendVec y n G x‖ ≤ eta

Every 1/2-Hölder forcing field is uniformly approximated on the cube by a continuous field on the closed cube with the same Hölder constant.

4. The countable family

theorem Algsuperdiff.Section5.Support.exists_countable_holder_approx {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) {K : ℝ} (hK : 0 ≤ K) : ∃ (t : Set C(↑(closedCubeAt y n), HCPolySupport.Vec d)), t.Countable ∧ (∀ G ∈ t, Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) K (extendVec y n G)) ∧ ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) K g → ∀ (eta : ℝ), 0 < eta → ∃ G ∈ t, ∀ x ∈ cubeSetAt y n, ‖g x - extendVec y n G x‖ ≤ eta

A single countable family of continuous fields on the closed cube approximates every 1/2-Hölder field with constant K uniformly on the cube, and every member of it has the same Hölder constant.

theorem Algsuperdiff.Section5.Support.exists_countable_normalizedForceAt_approx {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : ∃ (t : Set C(↑(closedCubeAt y n), HCPolySupport.Vec d)), t.Countable ∧ (∀ G ∈ t, NormalizedForceAt y n (extendVec y n G)) ∧ ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), NormalizedForceAt y n g → ∀ (eta : ℝ), 0 < eta → ∃ G ∈ t, ∀ x ∈ cubeSetAt y n, ‖g x - extendVec y n G x‖ ≤ eta

The countable family in the form the normalized forcing class uses.