High-contrast homogenization: Provider.Quenched.SmallContrastResponseUpper

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

Reabsorbed compact response bounds

This file converts the extended-nonnegative compact pre-Young estimates to real inequalities only after finite row and weak bounds have been supplied. It then absorbs the terminal energy and combines the primal and adjoint bounds at the calibrated Schur loads.

theorem HCPolySupport.HighContrast.Quenched.real_preYoung_of_compact {response energy defect C expo : ℝ} {row weak : ENNReal} (hresponse : 0 ≤ response) (hC : 0 ≤ C) (hexpo : 0 ≤ expo) (hrow : row ≠ ⊤) (hweak : weak ≠ ⊤) (hcompact : ENNReal.ofReal response ≤ ENNReal.ofReal C * ENNReal.ofReal √defect * (ENNReal.ofReal √defect + ENNReal.ofReal √energy + row ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √energy * (ENNReal.ofReal √energy + row ^ (1 / 2)) + ENNReal.ofReal C * weak) : response ≤ C * √defect * (√defect + √energy + √row.toReal) + C * expo * √energy * (√energy + √row.toReal) + C * weak.toReal

A finite compact pre-Young estimate has the corresponding real form. The explicit finiteness hypotheses prevent toReal ⊤ = 0 from weakening the claim.

theorem HCPolySupport.HighContrast.Quenched.centered_response_sup_le_of_reabsorbed_compact_preYoung {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) {S SStar K : Mat d} {C expo eta D L W Z : ℝ} (hC : 0 ≤ C) (hexpo : 0 ≤ expo) (hexpoOne : expo ≤ 1) (heta : 0 < eta) (hL : 0 ≤ L) (hW : 0 ≤ W) (habsorb : C * eta + 3 / 2 * C * expo ≤ 1 / 2) (tauMinus tauPlus EJMinus EJPlus centerMinus centerPlus : Vec d → ℝ) (rowMinus rowPlus weakMinus weakPlus : Vec d → ENNReal) (htauMinusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ tauMinus e) (htauPlusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ tauPlus e) (hEJMinusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ EJMinus e) (hEJPlusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ EJPlus e) (hcenterMinusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ centerMinus e) (hcenterPlusNonneg : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → 0 ≤ centerPlus e) (henergyMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → EJMinus e ≤ |Response.centeredResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e - Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| + centerMinus e) (henergyPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → EJPlus e ≤ |Response.centeredAdjointResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e + Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| + centerPlus e) (hpreYoungMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → ENNReal.ofReal |Response.centeredResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e - Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| ≤ ENNReal.ofReal C * ENNReal.ofReal √(tauMinus e) * (ENNReal.ofReal √(tauMinus e) + ENNReal.ofReal √(EJMinus e) + rowMinus e ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √(EJMinus e) * (ENNReal.ofReal √(EJMinus e) + rowMinus e ^ (1 / 2)) + ENNReal.ofReal C * weakMinus e) (hpreYoungPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → ENNReal.ofReal |Response.centeredAdjointResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e + Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| ≤ ENNReal.ofReal C * ENNReal.ofReal √(tauPlus e) * (ENNReal.ofReal √(tauPlus e) + ENNReal.ofReal √(EJPlus e) + rowPlus e ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √(EJPlus e) * (ENNReal.ofReal √(EJPlus e) + rowPlus e ^ (1 / 2)) + ENNReal.ofReal C * weakPlus e) (htauMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → tauMinus e ≤ D) (htauPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → tauPlus e ≤ D) (hrowMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → rowMinus e ≤ ENNReal.ofReal L) (hrowPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → rowPlus e ≤ ENNReal.ofReal L) (hweakMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → weakMinus e ≤ ENNReal.ofReal W) (hweakPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → weakPlus e ≤ ENNReal.ofReal W) (hcenterMinus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → centerMinus e ≤ Z) (hcenterPlus : ∀ (e : Fin d → ℝ), e ⬝ᵥ e = 1 → centerPlus e ≤ Z) : sSup ((fun (e : Vec d) => |Response.centeredResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e - Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| + |Response.centeredAdjointResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e + Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))|) '' {e : Vec d | e ⬝ᵥ e = 1}) ≤ 4 * C * ((3 / 2 + 1 / (4 * eta)) * D + L + W) + 2 * Z

Finite uniform profile bounds and the compact pre-Young estimates give a real bound for the calibrated primal--adjoint response supremum.