High-contrast homogenization: Provider.PolynomialHomogenization.Root.Dirichlet.FrameExponentFold

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

The response frame exponent, folded

The frame exponent of the response aggregation splits into the activation length and the outer sandwich bracket; the activation half folds into the eccentricity fold factor at the rate, and the bracket half is a factor in the sandwich radius alone.

This is the arithmetic content of the folded-scale response provider: after it, the only law-dependent quantity left in the response frame is the fold factor, which the bumped homogenization length pays for, and everything else is built from the dimension, the orders and the outer sandwich radius.

noncomputable def HCPolySupport.HighContrast.RowSupply.frameFoldConstant (d : ℕ) (g kappaRate J : ℝ) : ℝ

The law-free part of the folded frame constant: the activation constant at the collapsed order, times the outer bracket's contribution.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_frameExponent_le_fold {d : ℕ} {abar : Mat d} {g kappaRate : ℝ} {G L J : ℕ} {M : ℤ} (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) (hgeom : 0 < 1 - 3 ^ (-(2 * responseWindowOrder g - Certificate.printRowOrder g))) (hP : 0 < Certificate.shiftedTailAbsorptionPrefactor d (responseWindowOrder g) (Certificate.printRowOrder g) G) (hLeq : L = Certificate.formulaicNormalizedReferenceTailShift d (responseWindowOrder g) (Certificate.printRowOrder g) (2 * kappaRate) G) (hGupper : 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d)) (hMeq : M = max (max (↑L) (↑J + 1)) 1) : 3 ^ ((responseWindowOrder g - kappaRate) * ↑M + kappaRate * ↑L) ≤ frameFoldConstant d g kappaRate ↑J * eccentricityFoldFactor abar (Certificate.printRowOrder g * max (responseWindowOrder g) kappaRate / (2 * kappaRate * kappaRate)) ^ kappaRate

The frame exponent folds. The whole law dependence of the response frame exponent is the eccentricity fold factor raised to the rate; the remaining constant is built from the dimension, the orders and the bracket of the outer sandwich radius.