High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.EnergyPriceEccentricityCollapse

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

The Kenergy collapse and the order-uniform geometric factor

Two arithmetic facts the interface modules need and that nothing else supplies.

(1) The Kenergy collapse. read off, from the two definitions, that gaugeWitnessEnergyPriceW collapses to a law-free constant times E ^ (d + 2s + 2q); that reading needs lawFreeCubeEnergyConstantW's rpow squaring unfolded together with the gaugeWitnessEnergyPriceW product regrouping, none of whose definitional lemmas the energy modules exports." Both steps are done here. The squaring is (s ^ (−1/2)) ^ 2 = s⁻¹ for s > 0, and the window enters through Cwit ^ 2 + 1 ≤ (A ^ 2 + 1) · E ^ (2 q) at Cwit = A · E ^ q, E ≥ 1.

(2) The order-uniform geometric factor. witnessGeometricFactor d ρ r carries the order r = responseWindowOrder g, hence g. The frozen hole fixes C₀ : ℝ → ℝ → ℝ → ℝ before ∀ g, so no g-dependent factor may sit in C₀; and Lg is chosen before ρ, so no ρ-dependent factor may sit in Lg either. The escape is that witnessGeometricFactor is bounded, uniformly over the whole printed order window r ∈ [0, 1/2], by a function of (d, ρ) alone — which is inside C₀ s₀ ρ Rad's permitted dependence.

(1) The Kenergy collapse

theorem HCPolySupport.HighContrast.RowSupply.lawFreeCubeEnergyConstantW_eq (C : ℝ) (d : ℕ) {s : ℝ} (hs : 0 < s) (Cwit : ℝ) : EnergyPrice.lawFreeCubeEnergyConstantW C d s Cwit = C ^ 2 * s⁻¹ * (2 * ↑d * (Cwit ^ 2 + 1))

The law-free cube energy constant, unfolded: the rpow squaring is exact.

noncomputable def HCPolySupport.HighContrast.RowSupply.collapsedEnergyLawFree (C : ℝ) (d : ℕ) (s A : ℝ) : ℝ

The law-free part of the collapsed energy price.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.gaugeWitnessEnergyPriceW_le_collapsed {d : ℕ} (C : ℝ) {s A q : ℝ} (hs : 0 < s) (hq : 0 ≤ q) (hsd : 0 ≤ ↑d + 2 * s) (abar : Mat d) : EnergyPrice.gaugeWitnessEnergyPriceW C d s (A * max 1 (witnessEccentricity (symmPart abar)) ^ q) abar ≤ collapsedEnergyLawFree C d s A * max 1 (witnessEccentricity (symmPart abar)) ^ (↑d + 2 * s + 2 * q)

The Kenergy collapse, proved. At Cwit = A · E ^ q with E = max 1 (witnessEccentricity (symmPart abar)), the windowed gauge energy price is below a law-free constant times E ^ (d + 2 s + 2 q).

(2) The order-uniform geometric factor

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

The order-uniform geometric factor: a function of (d, ρ) alone.

Equations

• HCPolySupport.HighContrast.RowSupply.uniformWitnessGeometricFactor d rho = max 1 ((rho / (3 * √↑d)) ^ (-(1 / 2)))

theorem HCPolySupport.HighContrast.RowSupply.one_le_uniformWitnessGeometricFactor (d : ℕ) (rho : ℝ) : 1 ≤ uniformWitnessGeometricFactor d rho

theorem HCPolySupport.HighContrast.RowSupply.witnessGeometricFactor_le_uniform {d : ℕ} [NeZero d] {rho r : ℝ} (hrho : 0 < rho) (hr : 0 ≤ r) (hrHalf : r ≤ 1 / 2) : witnessGeometricFactor d rho r ≤ uniformWitnessGeometricFactor d rho

The geometric factor is bounded uniformly over the printed order window. witnessGeometricFactor d ρ r carries the order r, hence g; this bound removes both, at the cost of the worst case r = 1/2, and leaves a function of (d, ρ) — exactly C₀ s₀ ρ Rad's permitted dependence.