High-contrast homogenization: Provider.Regularity.FiniteLipschitzFluctuation #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized fluctuation of an affine approximation #
The normalized fluctuation of a scalar Sobolev function is bounded by its error from a specified affine function and by the Euclidean magnitude of the affine slope. This elementary estimate is independent of the multiscale finite-energy recurrence.
theorem
HCPolySupport.HighContrast.cubeLpNorm_two_cubeFluctuation_le_two_mul
{d : ℕ}
(Q : TriadicCube d)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q))
:
The normalized fluctuation of a square-integrable function is at most twice
its normalized L² norm.
theorem
HCPolySupport.HighContrast.normalized_fluctuation_le_affine_error_add_slope
{d : ℕ}
(Q : TriadicCube d)
(u : H1Function (openCubeSet Q))
(c : ℝ)
(e : Vec d)
:
cubeBesovScaleWeight 1 Q * cubeLpNorm Q 2 (cubeFluctuation Q u.toFun) ≤ 2 * (normalizedAffineCandidateError Q u.toFun c e + cubeBesovW12LocalPoincareConstant d * euclideanNorm e)
The normalized fluctuation is controlled by the error from a specified affine function and the Euclidean magnitude of its slope.