High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessHeadBound

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

(ii), part one: the scheduled head, dominated at an explicit constant

the hhead premise binder asks, for every J in the outer bracket, for

scheduledRateHead d
    √(hsAffineFactor S⁻¹ s ‖S‖) Cdual
    ((3 ^ b · foldedAnchoredFrameConstant …) ^ 2 · Kenergy) hardyConstant
  ≤ ENNReal.ofReal (C₀ s ρ Rad) .

This module discharges it at the explicit constant frozenWitnessHeadConstant, through real-valued bridge scheduledRateHead_le_ofReal and three factor bounds:

• the outputFactor_le_gaugeOutputLawFree_mul_fold premise — the ρ-paid output factor, with its eccentricity fold;
• the three_rpow_mul_foldedAnchoredFrameConstant_le premise — the flux split, whose square root needs the frame constant to be nonnegative; no lemma said so, and foldedAnchoredFrameConstant_nonneg supplies it here;
• any dominating KenergyBound — supplied from the modules named above at the call site.

The constant produced still carries abar, through the output factor's fold. That is deliberate and is what that module permits: C₀ is an internal parameter, chosen after abar is in scope; the hole's C₀, which must precede ∀ g, is reached in the next module by the constant_and_eccentricity_absorbed premise, which moves the eccentricity power into pEcc and the Lg-class residual into Lg.

The frame constant is nonnegative

theorem HCPolySupport.HighContrast.RowSupply.foldedAnchoredFrameConstant_nonneg (d : ℕ) {g kappaRate s Rad cnorm delta Jr : ℝ} (hg : g ∈ Set.Ico 0 1) (hs₀ : s ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hRad : 0 ≤ Rad) : 0 ≤ foldedAnchoredFrameConstant d g kappaRate s (coarseFluxResponseConstant d) Rad cnorm delta Jr

The folded anchored frame constant is nonnegative. Needed to split √(X² · Kenergy) as X · √Kenergy; no declaration stated it.

theorem HCPolySupport.HighContrast.RowSupply.three_rpow_mul_foldedAnchoredFrameConstant_nonneg (d : ℕ) {g kappaRate s Rad cnorm delta Jr : ℝ} (hg : g ∈ Set.Ico 0 1) (hs₀ : s ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hRad : 0 ≤ Rad) : 0 ≤ Real.rpow 3 (responseWindowOrder g) * foldedAnchoredFrameConstant d g kappaRate s (coarseFluxResponseConstant d) Rad cnorm delta Jr

The whole flux head of the frame constant is nonnegative.

The head constant

noncomputable def HCPolySupport.HighContrast.RowSupply.frozenWitnessHeadConstant (d : ℕ) (g kappaRate s rho Rad cnorm Cdual hardyReal KenergyBound : ℝ) (abar : Mat d) : ℝ

The constant at which the hhead premise is discharged. Its only abar dependence is the output factor's eccentricity fold.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.headProduct_mono {out out' Cdual Cb sq sq' hr : ℝ} (hout : out ≤ out') (hsq : sq ≤ sq') (hout0 : 0 ≤ out) (hCdual0 : 0 ≤ Cdual) (hCb0 : 0 ≤ Cb) (hsq0 : 0 ≤ sq) (hhr0 : 0 ≤ hr) : out * Cdual * (2 * (Cb * (sq * hr))) ≤ out' * Cdual * (2 * (Cb * (sq' * hr)))

Monotonicity of the scheduled head's real form in its two variable factors.

The head domination

theorem HCPolySupport.HighContrast.RowSupply.frozenWitnessScheduledHead_le {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {j : ℤ} {z : Vec d} {g kappaRate s rho Rad cnorm delta Jr Cdual hardyReal Kenergy KenergyBound : ℝ} {hardyConstant : ENNReal} (hS : Matrix.PosDef (symmPart abar)) (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappaRate) (hs₀ : s ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) (hRadpos : 0 < Rad) (hJr : 0 ≤ Jr) (hJB : 3 ^ Jr ≤ 1 + 3 * (2 * Rad)) (hdelta1 : √delta ≤ 1) (hCdual : 0 ≤ Cdual) (hhardyReal : 0 ≤ hardyReal) (hhardy : hardyConstant ≤ ENNReal.ofReal hardyReal) (hK0 : 0 ≤ Kenergy) (hKle : Kenergy ≤ KenergyBound) : scheduledRateHead d (√(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖)) Cdual ((Real.rpow 3 (responseWindowOrder g) * foldedAnchoredFrameConstant d g kappaRate s (coarseFluxResponseConstant d) Rad cnorm delta Jr) ^ 2 * Kenergy) hardyConstant ≤ ENNReal.ofReal (frozenWitnessHeadConstant d g kappaRate s rho Rad cnorm Cdual hardyReal KenergyBound abar)

(ii), part one. the hhead premise at the explicit frozenWitnessHeadConstant.