High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1FiniteFixedBaseDecay

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

One base minimizer on every intermediate cube

The exact minimizer chosen on the base cube is retained while the observation cube varies. Consecutive minimizer increments are propagated by the available quarter-power energy growth and summed against the available real-rate excess decay.

noncomputable def HCPolySupport.HighContrast.Root.finiteTrialGradientFieldLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) : Vec d →ₗ[ℝ] ↥(LocalGradientL2 d q)

Underlying local-gradient field of the finite trial harmonic gradient linear map.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Root.finiteTrialGradientResidual_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) (u : Book.Ch03.CubeSolution (originCube d ↑m) a) (b : Vec d) : have J := (finiteCubeSolutionRestriction a ⋯ u).toH1.gradToHilbertVectorL2; J - (finiteTrialGradientFieldLinearMap a hqm) b = (finiteAffineGradientResidual a ⋯ u b).toH1.gradToHilbertVectorL2

The trial-map residual is the restricted affine residual gradient class.

theorem HCPolySupport.HighContrast.Root.exists_scalarIdentityFiniteAffineFixedBaseDecayConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (hetaHalf : 1 / 2 ≤ eta) (heta1 : eta < 1) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℕ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta ↑n → ∀ (hnm2 : n + 2 ≤ m) (u : Book.Ch03.CubeSolution (originCube d ↑m) a), have bBase := finiteAffineExactMinimizer a ⋯ u; ∀ q ∈ Finset.Icc n m, (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a (↑m) bBase).toH1.grad x) ≤ ENNReal.ofReal (C * Real.rpow 3 (-eta * ↑(m - q))) * finiteAffineGradientExcess a (↑m) (↑m) u

The fixed base minimizer has the same real-rate decay on every intermediate centered cube.