High-contrast homogenization: Provider.Response.PreYoungRowPartialDischarge

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

Partial discharge of the pre-Young response rows

The terminal row energy is a localized weighted optimizer energy. Its measurability therefore follows from measurable selection for the canonical optimizer, leaving only a finite-integral domination premise. This closes the per-scale energy input of the primal and adjoint row estimates.

The cell-pairing bridge is insensitive to the chosen representative of the coefficient field. The pointwise estimates below select an everywhere elliptic representative internally and transport the doubled response field, coarse block, and energy average along almost-everywhere equality.

Measurability and integrability of the row energy

theorem HCPolySupport.HighContrast.Response.cellQuarterEnergy_eq_weightedOptimizerEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : cellQuarterEnergy hq k t w a p r = (MeasureTheory.volume (adaptedCell q t)).toReal * (MeasureTheory.volume (adaptedCellAt q k w)).toReal⁻¹ * Selection.weightedOptimizerEnergy (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r ((adaptedCellAt q k w).indicator fun (x : Vec d) => 1)

A child quarter-energy is a fixed multiple of the terminal optimizer energy localized to that child.

theorem HCPolySupport.HighContrast.Response.measurable_cellQuarterEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (p r : Vec d) : Measurable fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w a p r

The child quarter-energy is measurable on coefficient space.

theorem HCPolySupport.HighContrast.Response.cellQuarterEnergy_le_card_mul_responseJ {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : cellQuarterEnergy hq k t w a p r ≤ ↑(alignedIndex q k t).card * Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r

A single cell energy is bounded by the subdivision cardinality times the terminal response.

theorem HCPolySupport.HighContrast.Response.integrable_cellQuarterEnergy_of_integrable_responseJ {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (sample : CoeffSpace d → CoeffSpace d) (hsample : Measurable sample) (p r : Vec d) (hintJ : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((sample a).coeffOn (adaptedDomain hq t)) p r) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (sample a) p r) P

Integrability of the terminal response controls every measurable child quarter-energy.

theorem HCPolySupport.HighContrast.Response.integrable_cellQuarterEnergy_subSkew_of_finiteAdaptedMean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (a.subSkew g hg) p r) P

A finite adapted mean makes every constant-skew primal child energy integrable.

theorem HCPolySupport.HighContrast.Response.integrable_cellQuarterEnergy_adjointSubSkew_of_finiteAdaptedMean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (a.subSkew g hg).transpose p r) P

A finite adapted mean independently controls the coefficient-transpose child energy.

theorem HCPolySupport.HighContrast.Response.profileAnnealedCellEnergySq_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (w : Fin d → ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : 0 ≤ profileAnnealedCellEnergySq P hq k t w sample p r

Annealed child energies are nonnegative without an additional law premise.

Representative-independent cell pairings

theorem HCPolySupport.HighContrast.Response.abs_vecDot_averageVec_potential_coeffSpace_le {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (hpsd : Matrix.PosSemidef (Book.Ch02.coarseBlockMatrix U (a.coeffOn U)).lowerRight) (hdet : IsUnit (Matrix.det (Book.Ch02.coarseBlockMatrix U (a.coeffOn U)).lowerRight)) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U (a.coeffOn U) Y) (Qcen : Vec d) : |vecDot Qcen (Book.Ch02.averageVec U Y.potential)| ≤ √(Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField (a.coeffOn U) x) (Y.eval x))) * profileSchurLoadFlux (Book.Ch02.coarseBlockMatrix U (a.coeffOn U)) Qcen

The potential-slot cell pairing for a coefficient-space sample, with the everywhere-elliptic representative selected internally.

theorem HCPolySupport.HighContrast.Response.abs_vecDot_averageVec_flux_coeffSpace_le {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (hpsd : Matrix.PosSemidef (Book.Ch02.coarseBlockMatrix U (a.coeffOn U)).upperLeft) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U (a.coeffOn U) Y) (Pcen : Vec d) : |vecDot Pcen (Book.Ch02.averageVec U Y.flux)| ≤ √(Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField (a.coeffOn U) x) (Y.eval x))) * profileSchurLoadGradient (Book.Ch02.coarseBlockMatrix U (a.coeffOn U)) Pcen

The flux-slot cell pairing for a coefficient-space sample, with the everywhere-elliptic representative selected internally.

theorem HCPolySupport.HighContrast.Response.abs_vecDot_blockCellAverage_diagonalWeakState_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r Pcen Qcen : Vec d) : |vecDot Qcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r)).1| ≤ 2 * √(cellQuarterEnergy hq k t w a p r) * profileSchurLoadFlux (coarseBlock (adaptedCellAt q k w) a) Qcen ∧ |vecDot Pcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r)).2| ≤ 2 * √(cellQuarterEnergy hq k t w a p r) * profileSchurLoadGradient (coarseBlock (adaptedCellAt q k w) a) Pcen

The two cell-average pairings for the restricted diagonal optimizer. The pointwise elliptic representative is selected inside the proof, so the result applies directly to a coefficient-space sample and to its transpose.

Annealed cell pairings

theorem HCPolySupport.HighContrast.Response.half_integral_cellPairings_primal_le_of_integrable_energy {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hint : HasIntegrableCoarseBlock P (adaptedCellAt q k w)) (hintEnergy : MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (a.subSkew g hg) p r) P) : 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Qcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t (a.subSkew g hg) p r)).1| ∂P ≤ √(profileAnnealedCellEnergySq P hq k t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r) * profileSchurLoadFlux (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen ∧ 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Pcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t (a.subSkew g hg) p r)).2| ∂P ≤ √(profileAnnealedCellEnergySq P hq k t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r) * profileSchurLoadGradient (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

Annealed primal cell pairings are controlled by the square root of the localized optimizer energy and the corresponding annealed Schur loads.

theorem HCPolySupport.HighContrast.Response.half_integral_cellPairings_adjoint_le_of_integrable_energy {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hint : HasIntegrableCoarseBlock P (adaptedCellAt q k w)) (hintEnergy : MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (a.subSkew g hg).transpose p r) P) : 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Qcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)).1| ∂P ≤ √(profileAnnealedCellEnergySq P hq k t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r) * profileSchurLoadFlux (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen ∧ 1 / 2 * ∫ (a : CoeffSpace d), |vecDot Pcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)).2| ∂P ≤ √(profileAnnealedCellEnergySq P hq k t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r) * profileSchurLoadGradient (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

Annealed adjoint cell pairings obey the same estimate after transporting the transposed coefficient response through the hatted adjoint block.

theorem HCPolySupport.HighContrast.Response.avsum_cellPair_le_sqrt_avsum_energy_mul_load {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) (cellPair energy pathLoad : ι → ℝ) (load : ℝ) (henergy : ∀ z ∈ Z, 0 ≤ energy z) (hload : 0 ≤ load) (hpath : ∀ z ∈ Z, pathLoad z = load) (hcell : ∀ z ∈ Z, cellPair z ≤ √(energy z) * pathLoad z) : avsum Z cellPair ≤ √(avsum Z energy) * load

Averaging the cellwise Cauchy bounds over a finite row preserves the root-mean-square energy and a stationary common load.

theorem HCPolySupport.HighContrast.Response.six_mul_sharpCutoffCoefficient_le_adaptedCutoffDerivativeCoeff {d : ℕ} [NeZero d] : 6 * (32 * ↑d ^ 2 * smoothTransitionProfile.derivBound) ≤ adaptedCutoffDerivativeCoeff d

The common adapted derivative coefficient absorbs the scale conversion and the half-energy normalization of the sharp cutoff oscillation bound.

Closed primal and adjoint row estimates