High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenHeadClassSplit

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

(ii), part two: the head constant, split into the C₀, fold and Lg classes

that module discharges the hhead premise at frozenWitnessHeadConstant, which still carries abar (through the output factor's fold) and (g, κ) (through fluxLgFactor and the amplitude's Lg half). The clause permits abar only in pEcc and (g, κ) only in Lg, so the constant must be split.

This module performs that split, at the KenergyBound that module + that module produce:

frozenWitnessHeadConstant … (collapsedEnergyLawFree C d s (AC0 · ALg) · E^(d+2s+2q)) abar
  ≤ frozenHeadC0Factor C d s ρ Rad cnorm Cdual hardyReal
      · E ^ (d + 1 + q)
      · frozenHeadLgFactor d g κ

with E := max 1 (witnessEccentricity (symmPart abar)) and q := witnessErrorEccentricityExponent g κ. Three facts do the work:

• collapsedEnergyLawFree_mul_split — A ↦ C² s⁻¹ (2d(A²+1)) · … is submultiplicative in the split amplitude, because (AC0·ALg)² + 1 ≤ (AC0²+1)(ALg²+1);
• the order trim d + 2s + 2q ≤ d + 1 + 2q, from s < 1/2 — the same trim that module and that module use, and the reason pEcc may be (d, g, κ)-level;
• (d+1)/2 + (d+1+2q)/2 = d + 1 + q, which is exactly's "pEcc = the sum of the rate-leg and energy-leg exponents".

Nonnegativity of the two flux classes

theorem HCPolySupport.HighContrast.RowSupply.fluxC0Factor_nonneg (d : ℕ) {s₀ : ℝ} (hs₀ : 0 < s₀) (Rad cnorm : ℝ) : 0 ≤ fluxC0Factor d s₀ Rad cnorm

theorem HCPolySupport.HighContrast.RowSupply.fluxLgFactor_nonneg (d : ℕ) (g kappaRate : ℝ) : 0 ≤ fluxLgFactor d g kappaRate

The collapsed constant

theorem HCPolySupport.HighContrast.RowSupply.collapsedEnergyLawFree_nonneg (C : ℝ) (d : ℕ) {s : ℝ} (hs : 0 < s) (A : ℝ) : 0 ≤ collapsedEnergyLawFree C d s A

theorem HCPolySupport.HighContrast.RowSupply.collapsedEnergyLawFree_mul_split (C : ℝ) (d : ℕ) {s : ℝ} (hs : 0 < s) (A B : ℝ) : collapsedEnergyLawFree C d s (A * B) ≤ collapsedEnergyLawFree C d s A * (B ^ 2 + 1)

The collapsed law-free constant splits multiplicatively.

A square root of a power

theorem HCPolySupport.HighContrast.RowSupply.sqrt_rpow_eq {E : ℝ} (hE : 0 ≤ E) (t : ℝ) : √(E ^ t) = E ^ (t / 2)

The three classes of the head constant

noncomputable def HCPolySupport.HighContrast.RowSupply.frozenHeadC0Factor (C : ℝ) (d : ℕ) (s rho Rad cnorm Cdual hardyReal : ℝ) : ℝ

The C₀-slot class of the head constant: (d, s, ρ, Rad, cnorm)-level.

Equations

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

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

The Lg-slot class of the head constant: (d, g, κ)-level.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.frozenHeadLgFactor_nonneg (d : ℕ) (g kappaRate : ℝ) : 0 ≤ frozenHeadLgFactor d g kappaRate

theorem HCPolySupport.HighContrast.RowSupply.headSlot_mono {X Cb F v w hr : ℝ} (hvw : v ≤ w) (hX0 : 0 ≤ X) (hCb0 : 0 ≤ Cb) (hF0 : 0 ≤ F) (hhr0 : 0 ≤ hr) : X * (2 * (Cb * (F * v * hr))) ≤ X * (2 * (Cb * (F * w * hr)))

The monotone slot of the head constant.

The split

theorem HCPolySupport.HighContrast.RowSupply.frozenWitnessHeadConstant_le_classes {d : ℕ} (C : ℝ) {g kappaRate s rho Rad cnorm Cdual hardyReal : ℝ} {abar : Mat d} (hs : 0 < s) (hsHalf : s ≤ 1 / 2) (hCdual : 0 ≤ Cdual) : frozenWitnessHeadConstant d g kappaRate s rho Rad cnorm Cdual hardyReal (collapsedEnergyLawFree C d s (witnessAmplitudeC0Factor d rho Rad * witnessAmplitudeLgFactor d g kappaRate) * max 1 (witnessEccentricity (symmPart abar)) ^ (↑d + 2 * s + 2 * witnessErrorEccentricityExponent g kappaRate)) abar ≤ frozenHeadC0Factor C d s rho Rad cnorm Cdual hardyReal * max 1 (witnessEccentricity (symmPart abar)) ^ (↑d + 1 + witnessErrorEccentricityExponent g kappaRate) * frozenHeadLgFactor d g kappaRate

(ii), part two. The head constant from the modules named above, at the KenergyBound from the modules named above, is below the product of its C₀ class, a fixed eccentricity power, and its Lg class.