High-contrast homogenization: Provider.Regularity.CorrectorGradientTranslationStabilityWeakRow

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

Corrector-gradient translation stability from the weak corrector row

The average of a corrector gradient over a centered triadic cube and its average over a fixed displacement of that cube are compared by pairing the field against the displaced-cube test on the parent cube. The pairing is exactly the difference of the two averages, and it is bounded by the field's scale normalized negative Besov norm times the test's positive Besov norm. The latter is proportional to the square root of the relative displacement, which tends to zero along the centered exhaustion, so one scale-uniform bound for the weak row already gives translation stability of the averages.

The row is read on the affine-plus-corrector field rather than on the corrector gradient alone; the two differ by a constant, which cancels in the difference of averages.

theorem HCPolySupport.HighContrast.cubeAverageVec_eq_integral_normalizedCubeMeasure_of_integrable {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : MeasureTheory.Integrable F (normalizedCubeMeasure Q)) : cubeAverageVec Q F = ∫ (x : Vec d), F x ∂normalizedCubeMeasure Q

For an integrable vector field, the coordinatewise cube average is its Bochner integral against normalized cube measure.

The pairing identity

theorem HCPolySupport.HighContrast.integrableOn_cubeSet_of_memLp_two {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume

theorem HCPolySupport.HighContrast.cubeBesovPairing_cubeTranslationTest (d n : ℕ) (t : Vec d) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet (originCube d ↑(n + 1))) MeasureTheory.volume) (hsubT : translatedCubeSet (originCube d ↑n) t ⊆ cubeSet (originCube d ↑(n + 1))) : cubeBesovPairing (originCube d ↑(n + 1)) f (cubeTranslationTest d n t) = cubeAverage (originCube d ↑n) f - cubeAverage (originCube d ↑n) fun (y : Vec d) => f (y + t)

Pairing a field against the displaced-cube test on the parent cube returns exactly the difference between its average over the cube and its average over the displaced cube.

The pairing bound

theorem HCPolySupport.HighContrast.norm_cubeAverageVec_translate_sub_le_of_weakRow (d : ℕ) [NeZero d] (n : ℕ) (F : Vec d → Vec d) (t : Vec d) {s : ℝ} (hs : 0 < s) (hs2 : s < 1 / 2) {W : ℝ} (hW : 0 ≤ W) (hWle : W ≤ 3 ^ n) (htW : ∀ (i : Fin d), |t i| ≤ W) {J : ℕ} (hJ : 1 ≤ J) {N : ℝ} (hmem : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d ↑(n + 1)))) (hrow : cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑(n + 1)) s F ≤ N) : ‖(cubeAverageVec (originCube d ↑n) fun (x : Vec d) => F (x + t)) - cubeAverageVec (originCube d ↑n) F‖ ≤ N * cubeTranslationTestBound d n s W J

One scale-uniform bound for the weak corrector row controls the difference between the average of a field over a centered cube and its average over a fixed displacement of that cube.

Translation stability

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.tendsto_norm_integral_globalGradient_translate_sub_zero_of_weakRow {d : ℕ} [NeZero d] (Phi : NormalizedLocalH1Carrier d) (e t : Vec d) {s : ℝ} (hs : 0 < s) (hs2 : s < 1 / 2) (q0 : ℕ) (N : ℝ) (hN : ∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => e + Phi.globalGradientRepresentative x) ≤ N) : Filter.Tendsto (fun (n : ℕ) => ‖∫ (x : Vec d), Phi.globalGradientRepresentative (x + t) ∂normalizedCubeMeasure (originCube d ↑n) - ∫ (x : Vec d), Phi.globalGradientRepresentative x ∂normalizedCubeMeasure (originCube d ↑n)‖) Filter.atTop (nhds 0)

Translation stability of corrector-gradient cube averages. One scale-uniform bound for the weak corrector row of the affine-plus-corrector field makes the centered normalized cube averages of the corrector gradient and of its fixed translate asymptotically equal.