Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastCapsBundleRowIsotropy

High-contrast homogenization: Provider.Quenched.SmallContrastCapsBundleRowIsotropy #

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

The caps bundle's row half, at the split row caps #

The part of the row caps that is independent of the block parametrization.

profile_caps_bundle_entry_of_block_at_level (the cited theorem) delivers six clauses: two rows, two weak quantities, two centering caps. Only the rows call the row caps (the corresponding proof step, the corresponding proof step); the weak quantities go through profilePrimalWeakQuantity_le_weakValueSharp_of_block_at_level, whose statement names the inflated reference and therefore belongs to the family of modules built on the block parametrization.

So the honest split of work is: the row half can be repointed to the corresponding argument split caps now, and that is what this file does; the weak half is repointed by the wave. Duplicating the bundle's unchanged weak and centering clauses here would produce a module that the wave immediately obsoletes, so it is not done.

The isotropic entry caps bundle is assembled from caps_bundle_entry_rows_isotropy below plus the family's _of_block siblings, with no new mathematics.

What is Π-free here and what is not. The first summand of rowSplitConstant is dimension-only. The second, capsDeepConstant, still carries boundaryConst · 3^{g((t+G)-s)} — but multiplied by 3^{(3/2-g)((k₀-1)-s)}, which the gap s - k₀ drives below any prescribed tolerance at rate 3/2 - g > 1/2, for every g in the frozen range (the corresponding argument). Choosing that gap is the caller's tiltGap-shaped threshold.

source
noncomputable def HCPolySupport.HighContrast.Quenched.capsDeepConstant {d : ℕ} (Cd g : ℝ) (mAl : Mat d) (G : ℕ) (k0 s t : ℤ) :
ℝ

The deep-leg constant of the split row cap, as it appears at the bundle's window (s, t) and split scale k₀.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.capsDeepConstant_nonneg {d : ℕ} [Nonempty (Fin d)] {Cd g : ℝ} (hCd : 1 ≤ Cd) (hg : g ∈ Set.Ico 0 1) {mAl : Mat d} (hn : Matrix.PosDef mAl) (G : ℕ) (k0 s t : ℤ) :
    0 ≤ capsDeepConstant Cd g mAl G k0 s t
    source
    theorem HCPolySupport.HighContrast.Quenched.caps_bundle_entry_rows_isotropy {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {lAl : ℤ} (hl : ↑(kZero d) ≤ lAl) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {mAl : Mat d} (hn : Matrix.PosDef mAl) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (t : ℤ) {G : ℕ} (hDelta : 0 ≤ t + ↑G - 1 - sK) (hentry : sourceMomentTwo K ≤ 3 ^ (t + ↑G - sK)) {s : ℤ} (hst : s ≤ t) (hgeomS : ∀ k ≤ s, ∀ w ∈ Response.alignedIndex (roundedGrid lAl mAl) k s, adaptedCellAt (roundedGrid lAl mAl) k w ⊆ centeredCube d (t + ↑G)) {k0 : ℤ} {cIso : ℝ} (hcIso : 0 ≤ cIso) (hiso : ∀ (k : ℤ), k0 ≤ k → k ≤ s → ∀ w ∈ Response.alignedIndex (roundedGrid lAl mAl) k s, BlockMatLoewnerLE (annealedBlock P (adaptedCellAt (roundedGrid lAl mAl) k w)) (blockScale (1 + cIso) E)) (hint : HasFiniteAdaptedMean P (roundedGrid lAl mAl) t) {S0 SStar0 K0 : Mat d} (hS0 : Matrix.PosDef S0) (hStar0 : Matrix.PosDef SStar0) (hform : toFullBlockMat (adaptedMean P (roundedGrid lAl mAl) t) = schurBlock S0 SStar0 K0) {eps : ℝ} (hpos : 0 < eps) (heps1 : eps ≤ 1) (htr : ↑d * (schurHattedContrast S0 SStar0 - 1) ≤ eps) {kap : ℝ} (hkap0 : 0 ≤ kap) (hcomp : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid lAl mAl) t) X)) (e : Vec d) :
    e ⬝ᵥ e = 1 → Response.profilePrimalHattedEarlierRow P (roundedGrid lAl mAl) (Response.responseSkew K0) s (Response.profilePrimalCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).1 (Response.profilePrimalCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).2 ≤ ENNReal.ofReal (rowValue2Isotropy d (rowSplitConstant cIso (capsDeepConstant Cd g mAl G k0 s t)) kap eps) ∧ Response.profileAdjointHattedEarlierRow P (roundedGrid lAl mAl) (Response.responseSkew K0) s (Response.profileAdjointCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).1 (Response.profileAdjointCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).2 ≤ ENNReal.ofReal (rowValue2Isotropy d (rowSplitConstant cIso (capsDeepConstant Cd g mAl G k0 s t)) kap eps)

    The bundle's two row clauses, at the split row caps. The row constant is rowSplitConstant cIso (capsDeepConstant …): a dimension-only head plus a geometrically discounted deep leg.