High-contrast homogenization: Provider.Regularity.LiouvilleGradientGrowth #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Gradient growth of finite realizations of a Liouville solution #
This module completes the function-to-gradient Caccioppoli step in the reverse
Liouville argument. It chooses the exact finite-cube realizations of a frozen
Liouville pair and proves that their two-scale-inner weighted energies are
o(R^theta).
theorem
HCPolySupport.HighContrast.exists_scalarIdentityLiouvilleFiniteGradientGrowth
(d : ℕ)
[NeZero d]
(s : ℝ)
(hs : 0 < s)
(hs_lt : s < 1 / 2)
(a : Book.Ch02.TriadicCoeffFamily d)
(delta : ℝ)
(n : ℤ)
(hdelta : delta ≤ 1)
(hgood : ScalarIdentityGoodTail a s delta n)
{b : CoeffField d}
{theta : ℝ}
(hb : IsAELocallyUniformlyElliptic b)
(hcoeff :
∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] b)
{v : Vec d → ℝ}
{Dv : Vec d → Vec d}
(hv : MemLiouvilleClass b theta v Dv)
:
∃ (C : ℝ),
0 < C ∧ ∃ (u : (q : ℕ) → Book.Ch03.CubeSolution (originCube d ↑q) a),
(∀ (q : ℕ), (u q).toH1.toFun = v ∧ (u q).toH1.grad = Dv) ∧ Filter.Tendsto
(fun (q : ℕ) =>
ENNReal.ofReal ((√↑d * 3 ^ q) ^ (-theta) * finiteCenteredCubeSolutionEnergy a (↑q) (u q) (↑q - 2)))
Filter.atTop (nhds 0)
The Liouville-growth output: finite realizations preserving (v,Dv) pointwise
have inner weighted energy o(R^theta) along scale-matched triadic radii.