High-contrast homogenization: Provider.Regularity.LiouvilleFixedCubeSlope #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
A canonical slope on one fixed cube #
This module turns vanishing finite-affine excess for exact realizations of one global gradient into a slope whose joint corrector gradient is that gradient on the fixed inner cube.
theorem
HCPolySupport.HighContrast.exists_jointSlope_of_fixedCubeExcess
{d : ℕ}
[NeZero d]
{s : ℝ}
{a : Book.Ch02.TriadicCoeffFamily d}
{delta c : ℝ}
{n₀ : ℤ}
(hthreshold :
c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ),
delta ∈ Set.Ioc 0 c →
ScalarIdentityGoodTail a s delta n →
∀ (q t : ℕ),
n ≤ ↑q →
∀ (e : Vec d),
euclideanNorm e ≤ 2 * euclideanNorm
(cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad))
(hdelta : delta ∈ Set.Ioc 0 c)
(hgood : ScalarIdentityGoodTail a s delta n₀)
(hCauchy : FiniteAffineCorrectionLocalCauchy a)
(q : ℕ)
(hnq : n₀ ≤ ↑q)
(u : (j : ℕ) → Book.Ch03.CubeSolution (originCube d ↑(q + j + 2)) a)
(Dv : Vec d → Vec d)
(huGrad : ∀ (j : ℕ), (u j).toH1.grad = Dv)
(hexcess : Filter.Tendsto (fun (j : ℕ) => finiteAffineGradientExcess a (↑q) (↑(q + j + 2)) (u j)) Filter.atTop (nhds 0))
:
∃ (eLim : Vec d),
(finiteCubeSolutionRestriction a ⋯ (u 0)).toH1.gradToHilbertVectorL2 = (jointAffineFullGradientLinearMap a hCauchy q) eLim
On one fixed admissible cube, vanishing affine excess identifies the global gradient with the joint affine-corrector gradient at some slope.