High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.SuccessorParent

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

theorem HCPolySupport.HighContrast.successor_toFun_eq_correction_sub {d : ℕ} [NeZero d] (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d) : (finiteAffineSuccessorDifference a m e).toH1.toFun = fun (x : Vec d) => (finiteAffineCorrection a (m + 1) e).toFun x - (finiteAffineCorrection a m e).toFun x

theorem HCPolySupport.HighContrast.weight_pred_eq_three_mul {d : ℕ} (m : ℤ) : cubeBesovScaleWeight 1 (originCube d (m - 1)) = 3 * cubeBesovScaleWeight 1 (originCube d m)

noncomputable def HCPolySupport.HighContrast.successorInnerRestriction {d : ℕ} [NeZero d] (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d) : Book.Ch03.CubeSolution (originCube d (m - 1 - 2)) a

The successive finite affine difference restricted three centered scales inside its outer cube.

Equations

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

theorem HCPolySupport.HighContrast.exists_identitySuccessorParentL2Constant (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d), scalarIdentityWeakError a (printCertificateOrder g) m ≤ 1 → scalarIdentityWeakError a (printCertificateOrder g) (m + 1) ≤ 1 → cubeBesovScaleWeight 1 (originCube d (m - 1)) * cubeLpNorm (originCube d (m - 1)) 2 (finiteAffineSuccessorDifference a m e).toH1.toFun ≤ C * (scalarIdentityWeakError a (printCertificateOrder g) m + scalarIdentityWeakError a (printCertificateOrder g) (m + 1)) * euclideanNorm e

The two finite response value rows control the successor difference one scale inside its outer cube.