High-contrast homogenization: Entry.Multiscale.ResponseTransferSkeleton

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

Inputs for the proof of p.response.transfer (HCPoly/Entry/Statements/ResponseTransfer.lean)

Decomposition of the printed proof p.response.transfer of Proposition p.response.transfer into a DAG of lemmas whose statements are the content. The assembly itself is HCPolySupport.HighContrast.Entry.response_transfer (HCPoly/Entry/ResponseTransfer.lean), which imports this file.

Conventions (following p.scale.selection and HCPoly/Entry/Multiscale/ScaleSelection/):

• The antecedent clauses on (P, E, Ψ, K, Src, B, jStar, F, s, t) of p.response.transfer are bundled verbatim in the scaffold predicate RawOutput; the assembly unpacks its own binders into it and adds nothing.
• Every kernel chooses its Csrc before ε; the assembly takes the maximum of the kernel source constants and of the kernel Bresps, which is legitimate because the source premise and the B-threshold are monotone (RawOutput.mono, using 1 < K from CoarseEllipticityDagger.one_lt_growthWitness).
• No premise is added anywhere. In particular the gap obligation.a.CFS (HC Lemma 2.15's extra premise at p.response.transfer, never supplied by the paper) is NOT added to persistence_transfer_kernel; that kernel states exactly what the paper claims.
• The four kernels are the four unproved external inputs of the argument: ext.adapted.response with Step 3, ext.persistence.transfer with HC Lemma 2.15 and the eccentricity bound, the canonical comparison, and near e.response.canonical.imbalance. They are assumed, not gaps in the proof.
• Unused hypothesis binders of a statement are underscore-prefixed.
• Printed 𝐀hom_{m,Id} is adaptedMean P (1 : Mat d) m; printed Θ_m is annealedContrast P m; printed q is Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F).

RawOutput was declared here; it is now declared, verbatim and in this same namespace, in HCPoly/Entry/Response/Core/ResponseBlockObjects.lean, which this file imports. It had to move so that the imported files can state their lemmas over it. Nothing else about it changed, and R1's statement below is unchanged.

Auxiliary lemmas

theorem HCPolySupport.HighContrast.Multiscale.response_tolerances (d : ℕ) (_hd : 2 ≤ d) (δ : ℝ) (hδ : δ ∈ Set.Ioc 0 1) : ∃ (ηiso : ℝ) (δad : ℝ) (ηp : ℝ) (ηm : ℝ), ηiso ∈ Set.Ioo 0 1 ∧ δad ∈ Set.Ioc 0 1 ∧ ηp ∈ Set.Ioo 0 1 ∧ ηm ∈ Set.Ioo 0 1 ∧ ηp ≤ ηiso ∧ 1 - ηiso ≤ (1 + δad) ^ (-↑d) - ηm ∧ 3 * ((1 + ηiso) ^ 3 / (1 - ηiso) * (1 + δad) - 1) ≤ δ

Step 1 of p.response.transfer: tolerances from (d, δ) only. Hint: ηiso := δ/60, δad := δ/(120 d), ηm := δ/120, ηp := ηiso; Bernoulli for (1+δad)^(-d) ≥ 1 - d δad; (1+η)^3/(1-η) ≤ 1 + 7 η for η ≤ 1/60.

theorem HCPolySupport.HighContrast.Multiscale.adaptedCell_one (d : ℕ) (j : ℤ) : adaptedCell 1 j = centeredCube d j

The Euclidean adapted cell is the centered cube: matVecMul 1 = id.

theorem HCPolySupport.HighContrast.Multiscale.annealedContrast_eq (d : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (m : ℤ) : annealedContrast P m = blockContrast (adaptedMean P 1 m)

Θ_m = blockContrast 𝐀hom_{m,Id} (HCPoly/Setup/Moments.lean, adaptedMean; HCPoly/Entry/Geometry/RoundedGridBasic.lean, adaptedCell_one).

theorem HCPolySupport.HighContrast.Multiscale.RawOutput.mono {d : ℕ} {γ : ℝ} {S : SelectionData} {ε σ Cglob Cprof Csrc Csrc' : ℝ} {H : ℕ} {Bresp Bresp' : ℝ} {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {Src : CoeffSpace d → ℝ} {B : ℝ} {jStar : ℕ} {F : BlockMat d} {s t : ℤ} (hC : Csrc' ≤ Csrc) (hBr : Bresp' ≤ Bresp) (h : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ K Src B jStar F s t) : RawOutput d γ S ε σ Cglob Cprof Csrc' H Bresp' P E Ψ K Src B jStar F s t

The raw output is monotone in the source constant and the B-threshold (0 ≤ logb 3 (2K) since 1 < K, field one_lt_growthWitness of CoarseEllipticityDagger).

theorem HCPolySupport.HighContrast.Multiscale.blockScale_loewner_mono {d : ℕ} (A : BlockMat d) (hA : Book.Ch02.BlockPosDef A) {a b : ℝ} (hab : a ≤ b) : BlockMatLoewnerLE (blockScale a A) (blockScale b A)

Scalar monotonicity of blockScale in the Loewner order on a positive block.

theorem HCPolySupport.HighContrast.Multiscale.loewner_trans {d : ℕ} {A B C : BlockMat d} (h₁ : BlockMatLoewnerLE A B) (h₂ : BlockMatLoewnerLE B C) : BlockMatLoewnerLE A C

Transitivity of the Loewner order (may already exist in the CoarseGraining package).

theorem HCPolySupport.HighContrast.Multiscale.nat_le_ceil_of_le (ℓ : ℕ) (x : ℝ) (h : ↑ℓ ≤ x) : ↑ℓ ≤ ⌈x⌉

ℓ ≤ x in ℝ gives ℓ ≤ ⌈x⌉ in ℤ (Int.le_ceil, Int.cast_le).

EccentricityScaleDecay (gated external inputs)

theorem HCPolySupport.HighContrast.Multiscale.adapted_response_core (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δad ∈ Set.Ioc 0 1, ∃ (H : ℕ), max 4 S.h ≤ H ∧ ∀ (Cprof : ℝ), 0 < Cprof → ∃ σ₀ ∈ Set.Ioc 0 ε, ∀ σ ∈ Set.Ioc 0 σ₀, ∀ (Cglob : ℝ), 0 < Cglob → ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ K Src B jStar F s t → canonicalImbalance (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ≤ 1 + δad

R1 kernel ext.adapted.response: the adapted response estimate proper, exactly K1's third conjunct. It is the adapted response estimate the paper takes as given at e.response.adapted.conclusion; its proof is not part of this development.

The private copy of A12 blockPosDef_of_toFullBlockMat_posDef that stood here has been removed: HCPoly/Entry/Multiscale/Initial/ScalarBounds.lean declares it publicly in this same namespace, and it is now in this file's import graph (through HCPoly/Entry/Response/Core/ResponseBlockObjects.lean), so the private copy was a duplicate declaration. K1's proof below is unchanged and now uses the public A12, exactly the declaration the removed docstring named.

theorem HCPolySupport.HighContrast.Multiscale.adapted_response_kernel (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δad ∈ Set.Ioc 0 1, ∃ (H : ℕ), max 4 S.h ≤ H ∧ ∀ (Cprof : ℝ), 0 < Cprof → ∃ σ₀ ∈ Set.Ioc 0 ε, ∀ σ ∈ Set.Ioc 0 σ₀, ∀ (Cglob : ℝ), 0 < Cglob → ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ K Src B jStar F s t → IsSymmetricBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ∧ Book.Ch02.BlockPosDef (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ∧ canonicalImbalance (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ≤ 1 + δad

K1 ext.adapted.response + Step 3 (e.response.adapted.conclusion): the selected adapted block at t is symmetric, positive, and has canonical imbalance ≤ 1 + δad; H, σ₀, Bresp are the paper's, chosen in the order the paper states them. It is an assumed input: its proof needs the source estimate on adapted subcubes, ext.annealed.primal.adjoint, ext.reference.block.comparison and a.stationarity, none of which this development has.

theorem HCPolySupport.HighContrast.Multiscale.persistence_transfer_kernel (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δad ∈ Set.Ioc 0 1, ∀ ηp ∈ Set.Ioo 0 1, ∀ ηm ∈ Set.Ioo 0 1, ∀ (H : ℕ), max 4 S.h ≤ H → ∀ (Cprof : ℝ), 0 < Cprof → ∀ σ ∈ Set.Ioc 0 ε, ∀ (Cglob : ℝ), 0 < Cglob → ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∃ (Cresp : ℝ), 0 < Cresp ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ K Src B jStar F s t → canonicalImbalance (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ≤ 1 + δad → ∃ (ℓ : ℕ), 1 ≤ ℓ ∧ ↑ℓ ≤ Cresp * Real.logb 3 (2 + aspectRatio E) ∧ IsSymmetricBlockMat (adaptedMean P 1 (t + ↑ℓ)) ∧ BlockMatLoewnerLE (blockScale ((1 + δad) ^ (-↑d) - ηm) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t)) (adaptedMean P 1 (t + ↑ℓ)) ∧ BlockMatLoewnerLE (adaptedMean P 1 (t + ↑ℓ)) (blockScale (1 + ηp) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t))

K2 ext.persistence.transfer + HC Lemma 2.15 + e.global.selection.eccentricity (p.response.transfer): a Euclidean generation t + ℓ with 1 ≤ ℓ ≤ Cresp log₃(2+Π) whose block is sandwiched by ((1+δad)^{-d} - ηm) 𝐀hom_{t,q} and (1+ηp) 𝐀hom_{t,q}. It is an assumed input: the paper's proof of it uses HC Lemma 2.15, whose own coarsening premise this development does not supply, and this statement carries no such premise.

theorem HCPolySupport.HighContrast.Multiscale.canonical_comparison_kernel {d : ℕ} (_hd : 2 ≤ d) (A M : BlockMat d) (_hAs : IsSymmetricBlockMat A) (hA : Book.Ch02.BlockPosDef A) (_hMs : IsSymmetricBlockMat M) {ηiso δad : ℝ} (hη : ηiso ∈ Set.Ioo 0 1) (hδ : δad ∈ Set.Ioc 0 1) (hlo : BlockMatLoewnerLE (blockScale (1 - ηiso) A) M) (hhi : BlockMatLoewnerLE M (blockScale (1 + ηiso) A)) (himb : canonicalImbalance A ≤ 1 + δad) : canonicalImbalance M ≤ (1 + ηiso) ^ 3 / (1 - ηiso) * (1 + δad)

K3 the canonical comparison (p.response.transfer): a Loewner sandwich (1-η) A ≤ M ≤ (1+η) A transfers the canonical imbalance with factor (1+η)^3/(1-η). Deterministic.

theorem HCPolySupport.HighContrast.Multiscale.euclidean_contrast_bridge_kernel {d : ℕ} (_hd : 2 ≤ d) (A : BlockMat d) (_hAs : IsSymmetricBlockMat A) (_hA : Book.Ch02.BlockPosDef A) {x : ℝ} (_hx : 0 ≤ x) (h : canonicalImbalance A ≤ 1 + x) : blockContrast A - 1 ≤ 3 * x

K4 the Euclidean contrast bridge (near e.response.canonical.imbalance): contrast minus one is at most three times imbalance minus one; the factor three is the one the tolerances of Step 1 give. Deterministic.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_blockMatVecMul_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockScale c A) X) = c * blockVecDot X (blockMatVecMul A X)

Scalar dilation acts on the entire doubled quadratic form.

theorem HCPolySupport.HighContrast.Multiscale.blockPosDef_of_blockScale_le {d : ℕ} {A M : BlockMat d} {c : ℝ} (hc : 0 < c) (hA : Book.Ch02.BlockPosDef A) (h : BlockMatLoewnerLE (blockScale c A) M) : Book.Ch02.BlockPosDef M

A positive scalar dilation of a positive block that sits below M makes M positive.