High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardDataTolerance

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

The identification-data tolerance

The thresholds at which a weak-error row already carries the intrinsic slope, the scale-linear value growth and the weak gradient row.

These declarations read a triadic family alone: no coefficient representative and no ellipticity pair appears in any of them, so the normalized-gauge supply consumes them unchanged.

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorDataTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The threshold at which a weak-error row already carries the intrinsic slope and the scale-linear value growth.

Equations

• HCPolySupport.HighContrast.Root.rootCorrectorDataTolerance d s hs hs2 = Classical.choose ⋯

theorem HCPolySupport.HighContrast.Root.rootCorrectorData_spec (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : rootCorrectorDataTolerance d s hs hs2 ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 (rootCorrectorDataTolerance d s hs hs2) → ScalarIdentityGoodTail a s delta n → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d), HasIntrinsicNormalizedSlope e (finiteAffineCorrectionJointLocalLimit a hCauchy e) ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (q : ℕ), n.toNat ≤ q → cubeLpNorm (originCube d ↑q) 2 (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative ≤ C * 3 ^ q

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorWeakRowTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The threshold at which a weak-error row already carries the weak gradient row of the anchored corrector.

Equations

• HCPolySupport.HighContrast.Root.rootCorrectorWeakRowTolerance d s hs hs2 = Classical.choose ⋯

theorem HCPolySupport.HighContrast.Root.rootCorrectorWeakRow_spec (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : rootCorrectorWeakRowTolerance d s hs hs2 ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 (rootCorrectorWeakRowTolerance d s hs hs2) → ScalarIdentityGoodTail a s delta n → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d), ∃ (N : ℝ), 0 ≤ N ∧ ∀ (q : ℕ), n.toNat ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalGradientRepresentative x) ≤ N

noncomputable def HCPolySupport.HighContrast.Root.rootCorrectorSupplyTolerance (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : ℝ

The tolerance at which the construction, its value row and its weak gradient row are all available, at the order s.

Equations

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

theorem HCPolySupport.HighContrast.Root.rootCorrectorSupplyTolerance_pos (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs2 : s < 1 / 2) : 0 < rootCorrectorSupplyTolerance d s hs hs2