High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessLambdaRouteComposition

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

The λ-route composition at the frozen witness

With the witness-cube enclosure of HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.WitnessCubeEnclosure in hand, observationHomogenizationError_le_referencePowerTail_fixedParent applies at the frozen witness, and sqrt_observationParent_powerPrice_eq (FixedParentResponsePriceAlgebra) rewrites its square root into the exact product

Claw · 3 ^ ((s − κ) M − s j + κ N) · amplitude,
Claw = √(observationFillingCoefficient d λ abar · geometricDiscount (1−2s) 1 ⁻¹)

which is precisely the hErr binder shape of the frozen-witness energy price at the eccentricity-shaped Cwit.

The second theorem performs the frozen-witness assembly: it takes exactly domain surface (hU, hUsub), the provider's λ ∈ Icc 1 3 from the response-window tail, the reference tail, and the observation identification, and produces the parent generation together with the hErr bound.

noncomputable def HCPolySupport.HighContrast.RowSupply.lambdaRouteClaw (d : ℕ) (s epsilon : ℝ) (abar : Mat d) : ℝ

The law-free half of the λ-route constant: the filling coefficient against the geometric discount, under a square root.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.lambdaRouteClaw_nonneg (d : ℕ) (s epsilon : ℝ) (abar : Mat d) : 0 ≤ lambdaRouteClaw d s epsilon abar

theorem HCPolySupport.HighContrast.RowSupply.observationHomogenizationError_le_lambdaRoutePrice {d : ℕ} [NeZero d] {s epsilon amplitude kappa : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hepsilon : 0 < epsilon) (hAmplitude : 0 ≤ amplitude) (center : Vec d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (t : ℤ) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) (N K M : ℤ) (hNM : N ≤ M) (hKM : K ≤ M) (hTail : ScalarIdentityPowerTail aRef s amplitude kappa (3 ^ N)) (aObs : Book.Ch03.CoeffFamily d) (hObs : (aObs.coeffOn (originCube d K)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d K))] fun (x : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff epsilon a y - skewPart abar) (x + center)) (hEnclose : adaptedCellTranslate (epsilonAffineGrid epsilon abar) K (epsilon⁻¹ • matVecMul (matSqrt (symmPart abar)) center + adaptedCellCenter (epsilonAffineGrid epsilon abar) K 0) ⊆ adaptedCell (Selection.normalizedRoot (symmPart abar)) M) : Book.Ch02.HomogenizationErrorOnCube (originCube d K) s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) aObs 1 ≤ lambdaRouteClaw d s epsilon abar * (3 ^ ((s - kappa) * ↑M - s * ↑K + kappa * ↑N) * amplitude)

The λ-route composition at a fixed parent, in the price shape. The all-depth observation error on the target cube is below the λ-route product Claw · 3 ^ ((s − κ) M − s K + κ N) · amplitude.

theorem HCPolySupport.HighContrast.RowSupply.exists_witnessLambdaRouteError {d : ℕ} [NeZero d] {s kappa deltaScaled lambda : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hlambda : lambda ∈ Set.Icc 1 3) (a : CoeffSpace d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (t : ℤ) {j : ℤ} {z : Vec d} {U : Set (Vec d)} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) (L : ℕ) (n : ℤ) (hLn : ↑L ≤ n) (hTail : ScalarIdentityPowerTail aRef s (√deltaScaled) kappa (3 ^ ↑L)) (aObs : Book.Ch03.CoeffFamily d) (hObs : (aObs.coeffOn (originCube d j)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (x : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff lambda a y - skewPart abar) (x + matVecMul (matSqrt (symmPart abar))⁻¹ z)) : ∃ (M : ℤ), M = max (max n j) 1 ∧ n ≤ M ∧ j ≤ M ∧ 1 ≤ M ∧ Book.Ch02.HomogenizationErrorOnCube (originCube d j) s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) aObs 1 ≤ lambdaRouteClaw d s lambda abar * (3 ^ ((s - kappa) * ↑M - s * ↑j + kappa * ↑L) * √deltaScaled)

The frozen-witness λ-route bound. Exactly domain surface, the provider's bracket λ ∈ Icc 1 3, the reference tail and the observation identification produce the parent generation and the hErr bound from the modules named above, with Claw the λ-route's own filling constant.