High-contrast homogenization: Provider.Response.LinearOscillationDuality

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

Oscillation duality for a linear cell functional

A bounded test function with small cell oscillation pairs against an integrable field through the field's cell averages alone: writing the test function as the telescoping sum of its cube projections and pairing each residual against the next projection of the field, every term is a supremum bound for the residual times a normalized cell-average sum.

The estimate is recorded at the endpoint exponents: the test function is measured in L^∞ on each cell and the field only through the first power of its cell averages. This is the reading a linear functional of a gradient needs, because the cell averages of a gradient are exactly what coarse-grained data controls.

Endpoint pairing at one depth

theorem HCPolySupport.HighContrast.Response.cubeAverage_abs_cubeProjection_eq_cubeBesovCircDepthAverage {d : ℕ} (Q : TriadicCube d) (G : Vec d → ℝ) (j : ℕ) : (cubeAverage Q fun (x : Vec d) => |cubeProjection Q j G x|) = cubeBesovCircDepthAverage Q 1 G j

The normalized cell-average sum of a field is the cube average of the absolute value of its projection.

theorem HCPolySupport.HighContrast.Response.abs_cubeAverage_cubeProjection_mul_cubeProjectionResidual_le {d : ℕ} (Q : TriadicCube d) (f G : Vec d → ℝ) (j : ℕ) {K : ℝ} (hf : MeasureTheory.MemLp f 1 (normalizedCubeMeasure Q)) (hres : ∀ x ∈ cubeSet Q, |cubeProjectionResidual Q j f x| ≤ K) : |cubeAverage Q fun (x : Vec d) => cubeProjection Q (j + 1) G x * cubeProjectionResidual Q j f x| ≤ K * cubeBesovCircDepthAverage Q 1 G (j + 1)

Endpoint pairing at one depth: the projection of the field against the projection residual of the test function is bounded by the residual's supremum times the normalized cell-average sum at the next depth.

The finite-depth duality

theorem HCPolySupport.HighContrast.Response.cubeBesovCircPartialNorm_one_one_eq_sum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (G : Vec d → ℝ) (N : ℕ) : cubeBesovCircPartialNorm Q s 1 1 N G = ∑ j ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q s 1 G j

At the endpoint outer exponent the circ partial norm is the plain sum of its depth seminorms.

theorem HCPolySupport.HighContrast.Response.cubeBesovCircDepthSeminorm_one_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (G : Vec d → ℝ) (j : ℕ) : cubeBesovCircDepthSeminorm Q s 1 G j = cubeBesovCircDepthWeight Q s j * cubeBesovCircDepthAverage Q 1 G j

The depth seminorm at the endpoint inner exponent is the weight times the normalized cell-average sum.

theorem HCPolySupport.HighContrast.Response.abs_cubeBesovPairing_cubeProjection_le_mul_cubeBesovCircPartialNorm {d : ℕ} (Q : TriadicCube d) (f G : Vec d → ℝ) (N : ℕ) {s K : ℝ} (hK : 0 ≤ K) (hGInt : MeasureTheory.IntegrableOn G (cubeSet Q) MeasureTheory.volume) (hf : MeasureTheory.MemLp f 1 (normalizedCubeMeasure Q)) (hfTop : ∀ j < N, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) ⊤ (normalizedCubeMeasure R)) (hmean : cubeAverage Q f = 0) (hres : ∀ j < N, ∀ x ∈ cubeSet Q, |cubeProjectionResidual Q j f x| ≤ K * cubeBesovCircDepthWeight Q s (j + 1)) : |cubeBesovPairing Q f (cubeProjection Q N G)| ≤ K * cubeBesovCircPartialNorm Q s 1 1 N G

The finite-depth oscillation duality. A mean-zero test function whose depth-j projection residual is at most K times the depth-j+1 weight pairs against the depth-N projection of the field with constant K and the field's circ partial norm.

The duality at full depth

theorem HCPolySupport.HighContrast.Response.abs_cubeBesovPairing_le_mul_of_uniform_cubeBesovCircPartialNorm_bound {d : ℕ} (Q : TriadicCube d) (f G : Vec d → ℝ) {s K C W : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hGInt : MeasureTheory.IntegrableOn G (cubeSet Q) MeasureTheory.volume) (hfInt : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) (hf : MeasureTheory.MemLp f 1 (normalizedCubeMeasure Q)) (hfBound : ∀ x ∈ cubeSet Q, |f x| ≤ C) (hfTop : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) ⊤ (normalizedCubeMeasure R)) (hmean : cubeAverage Q f = 0) (hres : ∀ (j : ℕ), ∀ x ∈ cubeSet Q, |cubeProjectionResidual Q j f x| ≤ K * cubeBesovCircDepthWeight Q s (j + 1)) (hW : ∀ (N : ℕ), cubeBesovCircPartialNorm Q s 1 1 N G ≤ W) : |cubeBesovPairing Q f G| ≤ K * W

The oscillation duality. For a bounded mean-zero test function whose projection residuals obey the depth-weighted bound, the pairing against an integrable field is controlled by any uniform bound for the field's circ partial norms.