High-contrast homogenization: Provider.Regularity.CubeTranslationDualTest

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The displaced-cube test function

The difference of the indicator of a centered triadic cube and of its displacement, normalized by the volume ratio to the parent cube, is a mean-zero test whose pairing with a vector field reads exactly the difference between the field's average over the cube and its average over the displaced cube.

Its positive Besov norm is small for two independent reasons, and the two estimates are recorded separately.

• At every depth the oscillation is controlled by the volume of the set where the cube and its displacement disagree, which is proportional to the displacement relative to the cube side.
• Beyond the depth of the cube itself the test is close, in normalized L², to a test built from a displacement adapted to the triadic grid at that depth, and an adapted test has no oscillation at that depth at all. The error is proportional to the depth's own side length, so it decays geometrically.

Together the two make the Besov norm of the test proportional to the square root of the relative displacement, which is the whole content of the translation stability of cube averages.

noncomputable def HCPolySupport.HighContrast.cubeIndicatorDifference {d : ℕ} (c : ℝ) (S₁ S₂ : Set (Vec d)) : Vec d → ℝ

The scaled difference of two indicator functions.

Equations

• HCPolySupport.HighContrast.cubeIndicatorDifference c S₁ S₂ x = c * (S₁.indicator (fun (x : HCPolySupport.Vec d) => 1) x - S₂.indicator (fun (x : HCPolySupport.Vec d) => 1) x)

def HCPolySupport.HighContrast.setDisagreement {d : ℕ} (S₁ S₂ : Set (Vec d)) : Set (Vec d)

The set on which two sets disagree.

Equations

• HCPolySupport.HighContrast.setDisagreement S₁ S₂ = S₁ \ S₂ ∪ S₂ \ S₁

theorem HCPolySupport.HighContrast.measurable_cubeIndicatorDifference {d : ℕ} {c : ℝ} {S₁ S₂ : Set (Vec d)} (h₁ : MeasurableSet S₁) (h₂ : MeasurableSet S₂) : Measurable (cubeIndicatorDifference c S₁ S₂)

theorem HCPolySupport.HighContrast.abs_cubeIndicatorDifference_le {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (S₁ S₂ : Set (Vec d)) (x : Vec d) : |cubeIndicatorDifference c S₁ S₂ x| ≤ c * (setDisagreement S₁ S₂).indicator (fun (x : Vec d) => 1) x

theorem HCPolySupport.HighContrast.abs_cubeIndicatorDifference_le_const {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (S₁ S₂ : Set (Vec d)) (x : Vec d) : |cubeIndicatorDifference c S₁ S₂ x| ≤ c

theorem HCPolySupport.HighContrast.measurableSet_setDisagreement {d : ℕ} {S₁ S₂ : Set (Vec d)} (h₁ : MeasurableSet S₁) (h₂ : MeasurableSet S₂) : MeasurableSet (setDisagreement S₁ S₂)

theorem HCPolySupport.HighContrast.memLp_cubeIndicatorDifference {d : ℕ} {c : ℝ} (hc : 0 ≤ c) {S₁ S₂ : Set (Vec d)} (h₁ : MeasurableSet S₁) (h₂ : MeasurableSet S₂) (Q : TriadicCube d) (p : ENNReal) : MeasureTheory.MemLp (cubeIndicatorDifference c S₁ S₂) p (normalizedCubeMeasure Q)

Normalized measure of a disagreement set

theorem HCPolySupport.HighContrast.normalizedCubeMeasure_real_le_volume_div {d : ℕ} (Q : TriadicCube d) {G : Set (Vec d)} (hG : MeasureTheory.volume G ≠ ⊤) : (normalizedCubeMeasure Q).real G ≤ (MeasureTheory.volume G).toReal / cubeVolume Q

theorem HCPolySupport.HighContrast.cubeLpNorm_two_cubeIndicatorDifference_le {d : ℕ} (Q : TriadicCube d) {c : ℝ} (hc : 0 ≤ c) {S₁ S₂ : Set (Vec d)} (h₁ : MeasurableSet S₁) (h₂ : MeasurableSet S₂) (htop : MeasureTheory.volume (setDisagreement S₁ S₂) ≠ ⊤) : cubeLpNorm Q 2 (cubeIndicatorDifference c S₁ S₂) ≤ c * √((MeasureTheory.volume (setDisagreement S₁ S₂)).toReal / cubeVolume Q)

Oscillation against a normalized L² norm

theorem HCPolySupport.HighContrast.cubeBesovOscillation_two_le_two_mul_cubeLpNorm {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : cubeBesovOscillation Q 2 f ≤ 2 * cubeLpNorm Q 2 f

theorem HCPolySupport.HighContrast.cubeBesovOscillation_eq_zero_of_eq_on_cubeSet {d : ℕ} (R : TriadicCube d) {f : Vec d → ℝ} {gamma : ℝ} (hf : ∀ x ∈ cubeSet R, f x = gamma) : cubeBesovOscillation R 2 f = 0

A function that is constant on a cube has no oscillation there.

theorem HCPolySupport.HighContrast.cubeBesovOscillation_congr_on_cubeSet {d : ℕ} (R : TriadicCube d) {f g : Vec d → ℝ} (hfg : ∀ x ∈ cubeSet R, f x = g x) : cubeBesovOscillation R 2 f = cubeBesovOscillation R 2 g

Two functions that agree on a cube have the same oscillation there.

The displaced-cube test

noncomputable def HCPolySupport.HighContrast.cubeTranslationTest (d n : ℕ) (t : Vec d) : Vec d → ℝ

The mean-zero test that reads the difference between the average of a field over a centered triadic cube and its average over a fixed displacement of that cube.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.memLp_cubeTranslationTest (d n : ℕ) (t : Vec d) (Q : TriadicCube d) (p : ENNReal) : MeasureTheory.MemLp (cubeTranslationTest d n t) p (normalizedCubeMeasure Q)

The two depth estimates

The crude and the adapted depth estimate

theorem HCPolySupport.HighContrast.cubeTranslationTest_depthAverage_le_displacement (d n : ℕ) (t : Vec d) {W : ℝ} (hW : 0 ≤ W) (hWle : W ≤ 3 ^ n) (htW : ∀ (i : Fin d), |t i| ≤ W) (j : ℕ) : cubeBesovDepthAverage (originCube d ↑(n + 1)) 2 (cubeTranslationTest d n t) j ≤ 8 * ↑d * 3 ^ d * (W / 3 ^ n)

Every depth average of the displaced-cube test is controlled by the relative displacement.

theorem HCPolySupport.HighContrast.cubeTranslationTest_depthAverage_le_depth (d n : ℕ) (t : Vec d) (j : ℕ) (hj : 1 ≤ j) : cubeBesovDepthAverage (originCube d ↑(n + 1)) 2 (cubeTranslationTest d n t) j ≤ 24 * ↑d * 3 ^ d * (1 / 3) ^ j

Beyond the depth of the cube itself the depth averages of the displaced-cube test decay geometrically: the test is close to one whose displacement is adapted to the triadic grid at that depth, and an adapted test has no oscillation there.

The test has zero average and small dual test norm

theorem HCPolySupport.HighContrast.cubeAverage_cubeTranslationTest_eq_zero (d n : ℕ) (t : Vec d) (Q : TriadicCube d) (hsubA : cubeSet (originCube d ↑n) ⊆ cubeSet Q) (hsubT : translatedCubeSet (originCube d ↑n) t ⊆ cubeSet Q) : cubeAverage Q (cubeTranslationTest d n t) = 0

theorem HCPolySupport.HighContrast.cubeTranslationTest_dualTestNorm_le (d n : ℕ) (t : Vec d) (s : ℝ) (Q : TriadicCube d) (M : ℕ) (hsubA : cubeSet (originCube d ↑n) ⊆ cubeSet Q) (hsubT : translatedCubeSet (originCube d ↑n) t ⊆ cubeSet Q) : cubeBesovDualTestNorm Q s 2 2 M (cubeTranslationTest d n t) ≤ ∑ j ∈ Finset.range (M + 1), cubeBesovDepthWeight Q s j * √(cubeBesovDepthAverage Q 2 (cubeTranslationTest d n t) j)

The dual test norm of the displaced-cube test is bounded by the sum over depths of the weighted square roots of its depth averages.

Containment in the parent cube

theorem HCPolySupport.HighContrast.cubeSet_originCube_subset_succ (d n : ℕ) : cubeSet (originCube d ↑n) ⊆ cubeSet (originCube d ↑(n + 1))

theorem HCPolySupport.HighContrast.translatedCubeSet_originCube_subset_succ (d n : ℕ) (t : Vec d) {W : ℝ} (hWle : W ≤ 3 ^ n) (htW : ∀ (i : Fin d), |t i| ≤ W) : translatedCubeSet (originCube d ↑n) t ⊆ cubeSet (originCube d ↑(n + 1))

The explicit bound

noncomputable def HCPolySupport.HighContrast.cubeTranslationTestBound (d n : ℕ) (s W : ℝ) (J : ℕ) : ℝ

The explicit bound on the dual test norm of the displaced-cube test: a term proportional to the square root of the relative displacement, and a geometric tail in the depth at which the two are separated.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.cubeTranslationTestBound_pos (d : ℕ) [NeZero d] (n : ℕ) {s W : ℝ} (hs2 : s < 1 / 2) (J : ℕ) : 0 < cubeTranslationTestBound d n s W J

theorem HCPolySupport.HighContrast.cubeTranslationTest_dualTestNorm_le_bound (d n : ℕ) (t : Vec d) {s : ℝ} (hs2 : s < 1 / 2) {W : ℝ} (hW : 0 ≤ W) (hWle : W ≤ 3 ^ n) (htW : ∀ (i : Fin d), |t i| ≤ W) {J : ℕ} (hJ : 1 ≤ J) (M : ℕ) : cubeBesovDualTestNorm (originCube d ↑(n + 1)) s 2 2 M (cubeTranslationTest d n t) ≤ cubeBesovScaleWeight s (originCube d ↑(n + 1)) * cubeTranslationTestBound d n s W J

The dual test norm of the displaced-cube test is at most the cube's scale weight times the explicit bound.