High-contrast homogenization: Provider.Regularity.LiouvilleAdditiveConstant #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Recovering the additive constant #
The local analytic core of the last Liouville step: an H¹ function with
zero gradient on a centered cube is almost everywhere its cube average.
theorem
HCPolySupport.HighContrast.H1Function.ae_eq_integralAverage_of_gradToVectorL2_eq_zero
{d : ℕ}
(q : ℕ)
(w : H1Function (localGradientCube d q))
(hgrad : w.gradToVectorL2 = 0)
:
w.toFun =ᵐ[volumeMeasureOn (localGradientCube d q)] fun (x : Vec d) => integralAverage (localGradientCube d q) w.toFun
Zero weak gradient on a centered cube forces an H¹ representative to
equal its integral average almost everywhere.
theorem
HCPolySupport.HighContrast.eq_of_const_ae_eq_const_localGradientCube
{d : ℕ}
(q : ℕ)
{c c' : ℝ}
(h : (fun (x : Vec d) => c) =ᵐ[volumeMeasureOn (localGradientCube d q)] fun (x : Vec d) => c')
:
Two scalar constants which agree almost everywhere on a centered cube are equal.
theorem
HCPolySupport.HighContrast.ae_eq_volume_of_forall_localGradientCube_ae_eq
{d : ℕ}
{f g : Vec d → ℝ}
(h : ∀ (q : ℕ), f =ᵐ[volumeMeasureOn (localGradientCube d q)] g)
:
f =ᵐ[MeasureTheory.volume] g
Local almost-everywhere identities on every centered cube assemble to a global almost-everywhere identity.
theorem
HCPolySupport.HighContrast.exists_additiveConstant_of_common_jointSlope
{d : ℕ}
[NeZero d]
{a : Book.Ch02.TriadicCoeffFamily d}
{n : ℤ}
(hCauchy : FiniteAffineCorrectionLocalCauchy a)
(u : (p : ℕ) → Book.Ch03.CubeSolution (originCube d (↑p - 2)) a)
(v : Vec d → ℝ)
(huFun : ∀ (p : ℕ), (u p).toH1.toFun = v)
(e : Vec d)
(he :
∀ (q : ℕ),
n.toNat ≤ q →
(finiteCubeSolutionRestriction a ⋯ (u (q + 4))).toH1.gradToHilbertVectorL2 = (jointAffineFullGradientLinearMap a hCauchy q) e)
:
∃ (c : ℝ),
v =ᵐ[MeasureTheory.volume] fun (x : Vec d) =>
vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c
Equality of the Liouville gradient with one canonical joint-corrector gradient determines the Liouville value representative up to one global additive constant.