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

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

The response source-load bound

This file finishes the absolute-scale chain with the geometric inequality (1 + 3^{-k})^n ≤ 4 and the two-sided all-scale carrier bound response_allscale_abs: the two- sided maximum respAllScaleAbs satisfies E[A^Q] ≤ Cη, the analogue for the two-sided family of the one-sided all-scale maximum bound. It then begins the scalewise bound on the response source load respSourceLoad in terms of the Loewner order: the annealed block agrees with the block congruence, the quadratic form of a block scaling restricts to the upper-left and lower-right corners as claimed, the transpose of a skew matrix is its negation, and a translated adapted cell still carries a quadratic admissible measure. The module serves the response transfer p.response.transfer, the two-sided source-load estimate assembled from the all-scale carrier bound and the scalewise annealed-block comparison.

theorem HCPolySupport.HighContrast.Multiscale.add4_pow_le (Q : ℕ) (u v w x : ℝ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hw : 0 ≤ w) (hx : 0 ≤ x) : (u + v + w + x) ^ Q ≤ 3 ^ Q * (u ^ Q + v ^ Q + 3 ^ Q * (w ^ Q + x ^ Q + x ^ Q))

Four-term form of add3_pow_le, needed because the two-sided pathwise bound has the extra source summand.

theorem HCPolySupport.HighContrast.Multiscale.pathwise_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ Kg Src) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (F : BlockMat d) (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (ht : ↑jStar ≤ t) (hcube : adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t ⊆ centeredCube d (2 * ↑jStar)) (C₀ Cn Cs η : ℝ) (hC₀ : 0 < C₀) (hCn : 0 < Cn) (hCs : 0 < Cs) (hη : 0 < η) (X : CoeffSpace d → ℝ) (a : CoeffSpace d) (hXa : 0 < X a) (hpath : ∀ (mm : Mat d), Matrix.PosDef mm → ∀ (j : ℤ) (y : Vec d), adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mm) j y ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mm) j y) a) (blockScale (C₀ * √(‖mm‖ * ‖mm⁻¹‖) * X a * 3 ^ (γ * max (↑jStar - ↑j) 0)) E)) (hnormt : BlockMatLoewnerLE E (blockScale (Cn * aspectRatio E * √(‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖)) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t))) (hsrcsmall : Cs * aspectRatio E * (‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖) * 3 ^ (-(rhoMax d γ * (↑t - ↑jStar))) ≤ η ^ (1 / ↑(bigQ d γ))) : respAllScaleAbs P γ jStar F t a ≤ (⨆ j ∈ Set.Icc (↑jStar) t, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑t - ↑j)) * ⨆ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) j ∩ adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t, blockOpNorm (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) j t y a) ^ bigQ d γ) ^ (↑(bigQ d γ))⁻¹ + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t + C₀ * Cn / Cs * η ^ (1 / ↑(bigQ d γ)) * X a + η ^ (1 / ↑(bigQ d γ)) / Cs

The pathwise two-sided all-scale bound: the two branches combined through respAllScaleAbs_le_of_forall. respAllScaleAbs_aestronglyMeasurable_integrable (WeakEstimateAssembly.lean) needs the same pathwise majorant this gives. It is pathwise_bound_max with one extra summand, eta^{1/Q} / C_s, which is the whole cost of the lower Loewner side.

theorem HCPolySupport.HighContrast.Multiscale.response_allscale_abs (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) (Cs : ℝ) (_hCs : 0 < Cs) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ C * η

The two-sided carrier bound response_allscale_abs: E[A^Q] <= C eta for the TWO-SIDED all-scale maximum A = respAllScaleAbs (ResponseBlockObjects.lean).

The estimate is the two-sided analogue of the one-sided all-scale maximum bound: it carries respAllScaleAbs in place of respAllScaleMax, with the same binders, the same RawOutput, the same RespSourceSmall, and the same ∃ Csrc, 0 < Csrc ∧ ∃ C, 0 < C ∧ … shape.

Constant: C = 3^Q (2 + 3^Q ((C_0 C_n / C_s)^Q 2^Q + 2 / C_s^Q)), positive because C_0, C_n, C_s are. The extra 2 / C_s^Q over the one-sided constant is the whole price of the lower Loewner side (source_term_le).

Helpers for the source load bound

These lemmas support response_source_load_bound (p.response.transfer). They carry the whole of the printed argument that is downstream of the per-cell annealed-block estimate: nonnegativity of the source load, the split of the series at a scale-wise bound, the geometric summation (3/2 > 0), and the passage from a Loewner bound Ē(z+U_k; b) ≤ c M_0 to the two printed quadratic forms |b_{k,z}^{1/2}P|^2 and |(S_{*,k,z})^{-1/2}Q|^2. All are private.

theorem HCPolySupport.HighContrast.Multiscale.qform_fst {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (x : Vec d) : vecDot x (matVecMul A.upperLeft x) ≤ vecDot x (matVecMul B.upperLeft x)

The upper-left diagonal block inherits the Loewner order: testing A ≤ B on (x, 0) isolates x · A_{11} x ≤ x · B_{11} x. This is the first of the two printed quadratic forms of the source load (p.response.transfer, |b_{k,z}^{1/2}P|^2 = P · b_{k,z} P).

theorem HCPolySupport.HighContrast.Multiscale.qform_snd {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (x : Vec d) : vecDot x (matVecMul A.lowerRight x) ≤ vecDot x (matVecMul B.lowerRight x)

The lower-right diagonal block inherits the Loewner order: testing A ≤ B on (0, x). This is the second printed quadratic form, |(S_{*,k,z})^{-1/2}Q|^2 = Q · S_{*,k,z}^{-1} Q (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.blockScale_qform_upperLeft {d : ℕ} (c : ℝ) (B : BlockMat d) (x : Vec d) : vecDot x (matVecMul (blockScale c B).upperLeft x) = c * vecDot x (matVecMul B.upperLeft x)

A scalar dilation scales the upper-left quadratic form.

theorem HCPolySupport.HighContrast.Multiscale.blockScale_qform_lowerRight {d : ℕ} (c : ℝ) (B : BlockMat d) (x : Vec d) : vecDot x (matVecMul (blockScale c B).lowerRight x) = c * vecDot x (matVecMul B.lowerRight x)

A scalar dilation scales the lower-right quadratic form.

theorem HCPolySupport.HighContrast.Multiscale.blockSqrt_qform_blockVecDot {d : ℕ} {A : BlockMat d} (hA : Matrix.PosSemidef (toFullBlockMat A)) (Y : BlockVec d) : blockVecDot (blockMatVecMul (blockSqrt A) Y) (blockMatVecMul (blockSqrt A) Y) = blockVecDot Y (blockMatVecMul A Y)

M_0^{1/2} is a genuine square root of M_0 on the quadratic forms: this is what turns the printed mean bound |M_0^{1/2}Y^±|^2 ≤ C κ_s of e.response.load.and.mean (e.response.load.and.mean, the shape carried by RespLoadMean) into a bound on Y · M_0 Y.

theorem HCPolySupport.HighContrast.Multiscale.respM0_qform_split_canonicalMetric {d : ℕ} (F : BlockMat d) (Y : BlockVec d) : blockVecDot Y (blockMatVecMul (respM0 F) Y) = vecDot Y.1 (matVecMul (explicitCanonicalMetric F) Y.1) + vecDot Y.2 (matVecMul (explicitCanonicalMetric F)⁻¹ Y.2)

M_0 = diag(m, m^{-1}) splits the quadratic form into its two printed pieces (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.weight_eq (n : ℕ) : 3 ^ (-(3 / 2) * ↑n) = (3 ^ (-(3 / 2))) ^ n

The weight of L_s at scale k = s - n is the n-th power of 3^{-3/2}.

theorem HCPolySupport.HighContrast.Multiscale.respSourceLoad_le_scalewise {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s : ℤ) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) (K : ℕ → ℝ) (hK : ∀ (n : ℕ), 0 ≤ K n) (hsum : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * (4 * K n)) (hb : ∀ (n : ℕ), ∀ z ∈ triadicIndexBox d n, vecDot Y.1 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) b).upperLeft Y.1) ≤ K n ∧ vecDot Y.2 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) b).lowerRight Y.2) ≤ K n) : Summable (respSourceLoadSummand P jStar F s b Y) ∧ respSourceLoad P jStar F s b Y ≤ ∑' (n : ℕ), 3 ^ (-(3 / 2) * ↑n) * (4 * K n)

The scale-wise reduction of L_s (p.response.transfer). A bound K n on the two printed quadratic forms of the annealed block at every cell of generation k = s - n bounds the whole source load by the weighted series ∑ 3^{-3n/2} · 4 K n, as soon as that series converges. This is the exact form in which the printed split at k = j_* is meant to be used: K n need not be bounded in n, only summable against the weight. The same hypotheses make the generation summands of L_s summable, so that the tsum defining L_s is a genuine sum rather than the junk value of a divergent series; both conclusions are recorded.

The annealed shear bridge at a general adapted cell.

coarseBlockMatrix_sub_skew_eq_blockCongr is pathwise and carries the hypothesis HasQuadraticMu U a. The block below (i) discharges that hypothesis on every adapted cell, (ii) ports the finite-dimensional matrix-integration lemmas so that a constant block congruence passes through the entrywise integrals of annealedBlockOf, and (iii) assembles E[A(V; a ∓ g)] = G^t E[A(V; a)] G for an arbitrary adapted cell V, which is p.response.transfer at every subcell rather than only at U_t.

theorem HCPolySupport.HighContrast.Multiscale.hasQuadraticMu_adaptedCellTranslate {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffSpace d) : HasQuadraticMu (adaptedCellTranslate q j y) ↑↑a

HasQuadraticMu holds on every adapted cell for the qualitative coefficient carrier: the cell is a bounded open convex domain (affine image of an open cube), the sample has a pointwise elliptic a.e. representative there, and CG's convex-domain recovery package realizes the Mu infimum; Mu_congr_of_ae_eq returns the conclusion to the original representative.

noncomputable def HCPolySupport.HighContrast.Multiscale.sourceLoadEntrywiseMatrixIntegral {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) (f : CoeffSpace d → Matrix ι ι ℝ) : Matrix ι ι ℝ

Entrywise integral of a matrix-valued function.

Equations

• HCPolySupport.HighContrast.Multiscale.sourceLoadEntrywiseMatrixIntegral P f = Matrix.of fun (i j : ι) => ∫ (a : HCPolySupport.HighContrast.CoeffSpace d), f a i j ∂P

theorem HCPolySupport.HighContrast.Multiscale.ofFullBlockMat_fromBlocks_mk {d : ℕ} (A B C D : Mat d) : ofFullBlockMat (Matrix.fromBlocks A B C D) = { upperLeft := A, upperRight := B, lowerLeft := C, lowerRight := D }

theorem HCPolySupport.HighContrast.Multiscale.matTranspose_neg_of_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) : matTranspose (-g) = - -g