High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessAmplitudeLawFree

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

(i) The explicit law-free amplitude Alaw, split into the C₀ and Lg classes

that module reduced the fifth head factor to any law-free Alaw dominating the witness-route amplitude

A = lambdaRouteClaw d b λ abar · (witnessGeometricFactor d ρ b ·
      frameFoldConstant d g κ J) ,      b := responseWindowOrder g .

This module renders Alaw explicitly and splits it by slot, exactly as the flux-constant split gives:

• witnessAmplitudeC0Factor d ρ Rad — (d, ρ, Rad)-level, the C₀ slot;
• witnessAmplitudeLgFactor d g κ — (d, g, κ)-level, the Lg slot.

No factor lands in two classes and no factor sees abar. The three bounds are used exactly once each:

factor of A	trimmed by	slot
observationFillingCoefficient d λ abar, λ ∈ Icc 1 3
EnergyPrice.observationFillingCoefficient_le_of_residualWindow (E23) → max 1 (54 d² Rad)
C₀
(geometricDiscount (1 − 2b) 1)⁻¹	—	Lg (through g)
witnessGeometricFactor d ρ b	the witnessGeometricFactor_le_uniform premise	C₀
activationFoldConstant d g κ (max b κ)	—	Lg
max 1 (3 ^ ((b − κ)(J + 2)))	the max_one_rpow_three_bracket_le premise, at `3 ^ J ≤ 1 + 6
Rad|C₀`

The upper bracket is what this module contributes. The two neighbouring modules carry only 2 Rad ≤ 3 ^ J; the last row needs 3 ^ J ≤ 1 + 3 (2 Rad), which Entry.exists_pow_three_bracket produces at the same time.

The two classes

noncomputable def HCPolySupport.HighContrast.RowSupply.witnessAmplitudeC0Factor (d : ℕ) (rho Rad : ℝ) : ℝ

The C₀-slot half of the law-free witness amplitude: (d, ρ, Rad).

Equations

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

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

The Lg-slot half of the law-free witness amplitude: (d, g, κ).

Equations

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

The geometric gap of the response window

theorem HCPolySupport.HighContrast.RowSupply.geometricDiscount_responseWindow_pos {g : ℝ} (hg : g ∈ Set.Ico 0 1) : 0 < Book.Ch02.geometricDiscount (1 - 2 * responseWindowOrder g) 1

The response-window discount is positive on the printed g-window.

The amplitude bound

theorem HCPolySupport.HighContrast.RowSupply.witnessRouteAmplitude_le_classes {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {g kappaRate rho Rad lambda : ℝ} {J : ℕ} (hS : Matrix.PosDef (symmPart abar)) (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappaRate) (hlambda : lambda ∈ Set.Icc 1 3) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) (hJupper : 3 ^ ↑J ≤ 1 + 3 * (2 * Rad)) : lambdaRouteClaw d (responseWindowOrder g) lambda abar * (witnessGeometricFactor d rho (responseWindowOrder g) * frameFoldConstant d g kappaRate ↑J) ≤ witnessAmplitudeC0Factor d rho Rad * witnessAmplitudeLgFactor d g kappaRate

(i), closed. The witness-route amplitude is below the product of its two law-free classes, with no abar and no λ left.