High-contrast homogenization: Entry.Response.Core.CenteredEnergyIdentity

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

The centred-response energy comparison

This file proves the centred-response energy identity e.response.by.centered.energies. The key input is the printed matrix comparison e.matrix.block.comparison, F ≤ (1 + 6(θ - 1)) F♯, established at the skew correction h = h_t for which k - h = r_t is symmetric and the printed transpose step is the identity; the file also proves the Loewner, quadratic-form and positive-semidefiniteness facts the comparison needs along the way. It then packages the hypothesis bundles — RespCalibrated, RespCutoffBound, RespEnergyDefect, RespLoadBound, RespLoadMean, RespSourceSmall and RespWeakBound — that carry each stage of the decomposition of adapted_response_core into the next, and proves the centred-energy estimate itself from them.

The block comparison and the trace step

Two inputs of e.response.by.centered.energies:

• response_by_centered_energies_block_comparison, the printed matrix comparison e.matrix.block.comparison (near e.matrix.block.comparison) F <= (1+6(theta-1)) F^sharp, proved at the skew correction h = h_t, for which k - h = r_t is symmetric and the printed transpose step is an identity;
• response_by_centered_energies_loewner_of_trace, the passage from the trace estimate of p.response.transfer to the Loewner estimate b_t <= (1+c) S_*, through lambda_max <= tr on the positive semidefinite normalized defect.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_full_inv {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : (toFullBlockMat A)⁻¹ = Matrix.fromBlocks (schurSigma A)⁻¹ ((schurSigma A)⁻¹ * Matrix.conjTranspose (schurSkew A)) (schurSkew A * (schurSigma A)⁻¹) (schurSkew A * (schurSigma A)⁻¹ * Matrix.conjTranspose (schurSkew A) + A.lowerRight⁻¹)

The explicit Schur inverse of a symmetric positive block.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_qform {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) (x y : Vec d) : blockVecDot (x, y) (blockMatVecMul A (x, y)) = vecDot x (matVecMul (schurSigma A) x) + vecDot (y - matVecMul (schurSkew A) x) (matVecMul A.lowerRight (y - matVecMul (schurSkew A) x))

The Schur form of the block quadratic form.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_sharp_blocks {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d)) = { upperLeft := schurSkew A * (schurSigma A)⁻¹ * Matrix.conjTranspose (schurSkew A) + A.lowerRight⁻¹, upperRight := schurSkew A * (schurSigma A)⁻¹, lowerLeft := (schurSigma A)⁻¹ * Matrix.conjTranspose (schurSkew A), lowerRight := (schurSigma A)⁻¹ }

The blocks of the reflected inverse A^# = R A⁻¹ R.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_qform_sharp {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) (x y : Vec d) : blockVecDot (x, y) (blockMatVecMul (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d))) (x, y)) = vecDot x (matVecMul A.lowerRight⁻¹ x) + vecDot (y + matVecMul (matTranspose (schurSkew A)) x) (matVecMul (schurSigma A)⁻¹ (y + matVecMul (matTranspose (schurSkew A)) x))

The Schur form of the quadratic form of A^# = R A⁻¹ R.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_cross {θ a b n tw tLx β : ℝ} (hH : b + 25 * n ≤ a + (25 * tw + 10 * β + tLx)) (hF1 : a ≤ θ * b) (hF2 : tLx ≤ 4 * (θ * b) - 4 * b) (hF3 : tw ≤ θ * n) : a + (tw - 2 * β + tLx) ≤ (1 + 6 * (θ - 1)) * (b + n)

Scalar core of the printed block comparison e.matrix.block.comparison.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_block_comparison {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) (ho : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d))) A) {θ : ℝ} (hθ : 1 ≤ θ) (hle : MatLoewnerLE (respBlockB A) (θ • schurSigmaStar A)) : canonicalImbalance A ≤ 1 + 6 * (θ - 1)

e.matrix.block.comparison (near e.matrix.block.comparison) at the skew correction h = h_t, for which k - h = r_t is symmetric.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_psd_le_trace {d : ℕ} {P : Mat d} (hP : Matrix.PosSemidef P) (x : Vec d) : vecDot x (matVecMul P x) ≤ Matrix.trace P * vecDot x x

A positive semidefinite matrix is dominated by its trace.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_respSym_herm {d : ℕ} (A : BlockMat d) : Matrix.conjTranspose (respSym A) = respSym A

r_t is symmetric.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_rTr_posSemidef {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : (respSym A * A.lowerRight * respSym A).PosSemidef

r_t S_*^{-1} r_t is positive semidefinite.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_respBlockB_posDef {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : Matrix.PosDef (respBlockB A)

b_t is positive definite.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_respM_posDef {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : Matrix.PosDef (respM A)

m_t is positive definite.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_trace_conj {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : (matSqrt A.lowerRight * respBlockB A * matSqrt A.lowerRight).trace = (schurSigma A * A.lowerRight).trace + (respSym A * A.lowerRight * respSym A * A.lowerRight).trace

tr(R b_t R) = tr(S S_*^{-1}) + tr(r_t S_*^{-1} r_t S_*^{-1}), R = S_*^{-1/2}.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_trace_rTrT_nonneg {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : 0 ≤ (respSym A * A.lowerRight * respSym A * A.lowerRight).trace

tr(r_t S_*^{-1} r_t S_*^{-1}) ≥ 0.

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies_loewner_of_trace {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) (ho : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d))) A) {c : ℝ} (hc : (matSqrt A.lowerRight * respBlockB A * matSqrt A.lowerRight).trace - ↑d ≤ c) : MatLoewnerLE (respBlockB A) ((1 + c) • schurSigmaStar A)

From a trace bound on the normalized b_t to the Loewner bound b_t ≤ (1+c) S_*.

Decomposition of adapted_response_core, part 1: the predicate bundles and the

centred-energy estimate

The predicate bundles that carry the output of one step of the decomposition of adapted_response_core into the hypotheses of the next, together with the centred-energy estimate.

Bundles

def HCPolySupport.HighContrast.Multiscale.RespCalibrated {d : ℕ} (C : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) : Prop

The calibrated-block sandwich e.response.calibrated.blocks (e.response.calibrated.blocks): C^{-1} M_0 <= Ehat_t^± <= C kappa_t^{1/2} M_0 and Ehat_s^± <= C kappa_s^{1/2} M_0.

Equations

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

def HCPolySupport.HighContrast.Multiscale.RespEnergyDefect {d : ℕ} (C : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : Prop

The energy and defect bounds e.response.energy.and.defect (e.response.energy.and.defect).

Equations

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

def HCPolySupport.HighContrast.Multiscale.RespLoadMean {d : ℕ} (C : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : Prop

The load and mean bounds e.response.load.and.mean: |M_0^{1/2}x^±|^2 <= C kappa_s^{1/2} and |M_0^{1/2}Y^±|^2 <= C kappa_s.

Equations

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

def HCPolySupport.HighContrast.Multiscale.RespSourceSmall (d : ℕ) (γ C η : ℝ) (E F : BlockMat d) (jStar : ℕ) (s t : ℤ) : Prop

The source-smallness pair e.response.source.smallness (e.response.source.smallness), with Pi = aspectRatio E and e(m)^2 = ‖m‖ ‖m⁻¹‖ for m = explicitCanonicalMetric F.

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respSourceLoadSummand {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s : ℤ) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) (n : ℕ) : ℝ

The generation-n summand of the source load L_s (p.response.transfer): the printed weight 3^{-3n/2} times the flat average over the generation-(s-n) cells of (|b_{s-n,z}^{1/2} P| + |(S_{*,s-n,z})^{-1/2} Q|)^2. respSourceLoad is the sum of this family over n.

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.respSourceLoad_eq_tsum_summand {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s : ℤ) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) : respSourceLoad P jStar F s b Y = ∑' (n : ℕ), respSourceLoadSummand P jStar F s b Y n

The source load is the sum of its generation summands.

def HCPolySupport.HighContrast.Multiscale.RespLoadBound {d : ℕ} (C : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : Prop

The source-load bound L_s^± <= C kappa_s^{3/2} (p.response.transfer). -- READING: kappa_s^{3/2} is written (sqrt kappa_s)^3.

The two summability conjuncts are not decoration. respSourceLoad is a tsum, whose value on a non-summable family is 0, and the two inequalities above then hold vacuously; the estimate of e.response.cutoff.estimate divides by L_s^± in the sense that it pairs against it, and is false at the junk value. The printed proof of the bound establishes convergence on the way ("the series converges because gamma < 3/2"), so the summability belongs here, where L_s^± is produced.

Equations

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

def HCPolySupport.HighContrast.Multiscale.RespWeakBound (C : ℝ) (CH : ℕ → ℝ) (d : ℕ) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (H : ℕ) (η : ℝ) (s t : ℤ) (e : Vec d) : Prop

The weak-norm estimate e.response.weak.estimate: (W^±)^{1/2} <= C (3^{-alpha H} + C_H eta^{1/(2Q)}) kappa_s^{1/2}.

Equations

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

def HCPolySupport.HighContrast.Multiscale.RespCutoffBound {d : ℕ} (C : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (H : ℕ) (s t : ℤ) (e : Vec d) : Prop

The cutoff estimate e.response.cutoff.estimate.

Equations

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

The centred-energy estimate

theorem HCPolySupport.HighContrast.Multiscale.response_by_centered_energies (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) (ε σ Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (_raw : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t) (M : ℝ) (_hM : ∀ (e : Vec d), vecDot e e = 1 → |respCenteredJMinus P jStar F t e| + |respCenteredJPlus P jStar F t e| ≤ M) : respKappa P jStar F t - 1 ≤ 12 * ↑d * M

The centred-energy estimate e.response.by.centered.energies: kappa_t - 1 <= 12 d sup_{|e|=1}(|Jtilde^-(e)| + |Jtilde^+(e)|), stated with an explicit bound M instead of a supremum.

Route: the trace identity of p.response.transfer (response_by_centered_energies_aux_centered_sum and response_by_centered_energies_aux_basis_trace), both trace terms nonnegative (p.response.transfer, response_by_centered_energies_trace_rTrT_nonneg), the passage from the trace estimate to the Loewner estimate b_t <= (1 + d M) S_* (response_by_centered_energies_loewner_of_trace), and then e.matrix.block.comparison (e.matrix.block.comparison) with h = h_t.

-- READING: the docstring of Analysis.schurSigma_le_corrected together with coupled_schur_le as the in-tree form of e.matrix.block.comparison. That is not what those two prove: coupled_schur_le goes from an imbalance bound to a corrected-Schur bound, i.e. the converse implication, and the only 6 in this direction is the aspect-ratio six of Analysis.refBlock_le_six_aspectRatio_smul_swapConj. The printed F <= (1+6(theta-1)) F^sharp is therefore proved here from scratch, at h = h_t, as response_by_centered_energies_block_comparison.

The printed 12 d is 2 * 6 * d: this proof gives kappa_t - 1 <= 6 d M, and M >= 0 supplies the remaining factor two.