High-contrast homogenization: Provider.Response.ProfileRowMeanEstimates

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

The cutoff-defect mean rows of the pre-Young estimate

The pre-Young assembly controls the two annealed means E[((φ-1)∇v_t)_{U_t}] and E[((φ-1)a∇v_t)_{U_t}], paired against the two annealed optimizer centers. Each pairing is bounded by a defect root times the scale-s Schur load, plus a scale gain times the energy root times the root of the all-earlier Schur row.

This file records the two annealed means, the two halves of the Schur load, the place of the scale-s load inside the all-earlier row, and the combination of the two mean estimates into the single boundary-mean term of the assembly.

A normalized-average Cauchy-Schwarz inequality

theorem HCPolySupport.HighContrast.Response.avsum_sqrt_le_sqrt_avsum {ι : Type u_1} {Z : Finset ι} {f : ι → ℝ} (hZ : Z.Nonempty) (hf : ∀ z ∈ Z, 0 ≤ f z) : (avsum Z fun (z : ι) => √(f z)) ≤ √(avsum Z f)

The normalized average of a square root is at most the square root of the normalized average.

theorem HCPolySupport.HighContrast.Response.avsum_weighted_le_sqrt_two_mul_defect {ι : Type u_1} {Z : Finset ι} {defect pairing weight : ι → ℝ} {tau load : ℝ} (hZ : Z.Nonempty) (hload : 0 ≤ load) (hdefect : ∀ z ∈ Z, 0 ≤ defect z) (hweight : ∀ z ∈ Z, |weight z| ≤ 1) (hpairing : ∀ z ∈ Z, |pairing z| ≤ √(defect z) * load) (htau : avsum Z defect = 2 * tau) : (avsum Z fun (z : ι) => |weight z * pairing z|) ≤ √(2 * tau) * load

The defect half of a cutoff-defect mean row. A family of cell pairings, each bounded by the root of a cell energy defect times a fixed load, has normalized average at most the root of the total defect times that load, once the cutoff weights are bounded by one. The total defect is twice the response defect.

The two halves of the Schur load

noncomputable def HCPolySupport.HighContrast.Response.profileSchurLoadFlux {d : ℕ} (H : BlockMat d) (Qcen : Vec d) : ℝ

The flux half |σ_bar_*^{-1/2}Q| of the Schur load.

Equations

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

noncomputable def HCPolySupport.HighContrast.Response.profileSchurLoadGradient {d : ℕ} (H : BlockMat d) (Pcen : Vec d) : ℝ

The gradient half |b_bar^{1/2}P| of the Schur load.

Equations

• HCPolySupport.HighContrast.Response.profileSchurLoadGradient H Pcen = HCPolySupport.Book.Ch02.vecNorm (HCPolySupport.matVecMul (HCPolySupport.HighContrast.matSqrt H.upperLeft) Pcen)

theorem HCPolySupport.HighContrast.Response.profileSchurLoadFlux_nonneg {d : ℕ} (H : BlockMat d) (Qcen : Vec d) : 0 ≤ profileSchurLoadFlux H Qcen

theorem HCPolySupport.HighContrast.Response.profileSchurLoadGradient_nonneg {d : ℕ} (H : BlockMat d) (Pcen : Vec d) : 0 ≤ profileSchurLoadGradient H Pcen

theorem HCPolySupport.HighContrast.Response.profileSchurLoad_eq_add_sq {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) : profileSchurLoad H Pcen Qcen = (profileSchurLoadFlux H Qcen + profileSchurLoadGradient H Pcen) ^ 2

The Schur load is the square of the sum of its two halves.

theorem HCPolySupport.HighContrast.Response.sqrt_profileSchurLoad {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) : √(profileSchurLoad H Pcen Qcen) = profileSchurLoadFlux H Qcen + profileSchurLoadGradient H Pcen

The root of the Schur load splits: the two halves add to the root.

The scale-s cell inside the all-earlier row

theorem HCPolySupport.HighContrast.Response.zero_mem_adaptedCell {d : ℕ} (q : Mat d) (j : ℤ) : 0 ∈ adaptedCell q j

The origin lies in every adapted cell.

theorem HCPolySupport.HighContrast.Response.adaptedCellAt_zero {d : ℕ} (q : Mat d) (j : ℤ) : adaptedCellAt q j 0 = adaptedCell q j

The aligned adapted cell at the zero label is the adapted cell.

theorem HCPolySupport.HighContrast.Response.alignedIndex_self {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) : alignedIndex q j j = {0}

The aligned index of a scale against itself is the single zero label.

theorem HCPolySupport.HighContrast.Response.avsum_alignedIndex_self {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (f : (Fin d → ℤ) → ℝ) : avsum (alignedIndex q j j) f = f 0

A normalized average over the aligned index of a scale against itself is the value at the zero label.

theorem HCPolySupport.HighContrast.Response.profilePrimalHattedRowPartial_self {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : profilePrimalHattedRowPartial P q h s s Pcen Qcen = profileSchurLoad (profileHattedBlock h (adaptedMean P q s)) Pcen Qcen

The lower-cutoff hatted row taken at the terminal cutoff is exactly the scale-s Schur load.

theorem HCPolySupport.HighContrast.Response.profileAdjointHattedRowPartial_self {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : profileAdjointHattedRowPartial P q h s s Pcen Qcen = profileSchurLoad (profileHattedAdjointBlock h (adaptedMean P q s)) Pcen Qcen

The same statement for the coefficient-transpose row.

theorem HCPolySupport.HighContrast.Response.profileSchurLoad_le_profilePrimalHattedEarlierRow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : ENNReal.ofReal (profileSchurLoad (profileHattedBlock h (adaptedMean P q s)) Pcen Qcen) ≤ profilePrimalHattedEarlierRow P q h s Pcen Qcen

The scale-row order: the scale-s Schur load is dominated by the primal all-earlier hatted row, because the scale-s row is the single cell U_s.

theorem HCPolySupport.HighContrast.Response.profileSchurLoad_le_profileAdjointHattedEarlierRow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : ENNReal.ofReal (profileSchurLoad (profileHattedAdjointBlock h (adaptedMean P q s)) Pcen Qcen) ≤ profileAdjointHattedEarlierRow P q h s Pcen Qcen

The coefficient-transpose scale-row order.

theorem HCPolySupport.HighContrast.Response.sqrt_profileSchurLoad_le_profilePrimalHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : ENNReal.ofReal √(profileSchurLoad (profileHattedBlock h (adaptedMean P q s)) Pcen Qcen) ≤ profilePrimalHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The root of the scale-s Schur load is dominated by the root of the primal all-earlier hatted row.

theorem HCPolySupport.HighContrast.Response.sqrt_profileSchurLoad_le_profileAdjointHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (h : Mat d) (s : ℤ) (Pcen Qcen : Vec d) : ENNReal.ofReal √(profileSchurLoad (profileHattedAdjointBlock h (adaptedMean P q s)) Pcen Qcen) ≤ profileAdjointHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The coefficient-transpose form of the scale-row root order.

The annealed cutoff-defect means

noncomputable def HCPolySupport.HighContrast.Response.profilePrimalCutoffMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (cut : Vec d → ℝ) (p r : Vec d) : BlockVec d

The annealed cutoff-defect mean E[((φ-1)X_t)_{U_t}] of the primal doubled optimizer state, taken slotwise.

Equations

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

noncomputable def HCPolySupport.HighContrast.Response.profileAdjointCutoffMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (cut : Vec d → ℝ) (p r : Vec d) : BlockVec d

The annealed cutoff-defect mean of the coefficient-transpose doubled optimizer state.

Equations

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

The boundary-mean term