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

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

Scale decay and eccentricity bounds for the response kernels

This file proves the support lemmas behind the two kernel inputs of the response transfer, adapted_response_kernel and persistence_transfer_kernel, consumed at Steps 3 and 4 of p.response.transfer. It shows a response block satisfies a geometric scale-decay bound whenever its Loewner order decays across scales, produces an eccentricity gap from a bound on the response block, and proves the Loewner comparisons for the block-scale difference and for the swapped conjugate at a bounded canonical imbalance, together with the antitonicity of the swapped-conjugate inverse under that order. A short adjoining module also restates the Euclidean-versus-adapted comparisons of AdaptedEuclideanComparison with the paper's unused unit-range hypothesis put back, for direct citation. Nothing else here is specific to either kernel.

Response inputs — the analytic kernels

• E1/E2: HC Lemma 2.15, re-derived at the rounded grid q = explicitRoundedGrid jStar m with a C(d,γ) and every binder witnessed. HC's a.CFS premise is unused by the proof; the fine-grid Euclidean adapter supplies the concentration input from the unit-range law. Consumed at p.response.transfer, with the source term normalized by p.response.transfer (𝐄 ≤ C(d,γ) Π 𝔢(m) 𝐀hom_{t,q}, i.e. adaptedMean_refBlock_normalization) and the HC source factor (1 + K² 3^{-t})^γ ≤ 2 absorbed into Csrc exactly as adaptedMean_refBlock_normalization absorbs it (⌈Csrc log₃(2K)⌉ ≤ j_*). Here 𝔢(m)² = ‖m‖‖m⁻¹‖.

theorem HCPolySupport.HighContrast.Multiscale.euclidean_le_adapted_comparison (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ) (C : ℝ), 0 < Csrc ∧ 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (t : ℤ), ↑jStar ≤ t → adaptedCell (Geometry.explicitRoundedGrid jStar m) t ⊆ centeredCube d (2 * ↑jStar) → ∀ (ℓ : ℕ), 1 ≤ ℓ → BlockMatLoewnerLE (adaptedMean P 1 (t + ↑ℓ)) (blockScale (1 + C * aspectRatio E * (‖m‖ * ‖m⁻¹‖) * 3 ^ (-↑ℓ)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) t))

E1 kernel: Euclidean-by-adapted comparison (HC's e.Euc.by.tilt, at the rounded grid; p.response.transfer, first inequality): for ℓ ≥ 1, 𝐀hom_{t+ℓ,Id} ≤ (1 + C Π ‖m‖‖m⁻¹‖ 3^{-ℓ}) 𝐀hom_{t,q}. Proof route (HC): use maximal adapted cells capped at t to tile □_{t+ℓ} up to a null set. Integer stationarity identifies the cap with adaptedMean P q t. Every lower row has relative volume ≤ C(d) 𝔢(m) 3^{j-(t+ℓ)} and is controlled by the source bound. Fine cells are recentered into the source window; the inverse-norm bound two makes this source estimate independent of eccentricity. The geometric series and adaptedMean_refBlock_normalization then give the result. This uses only stationarity and dagger; the stated unit-range assumption is unnecessary.

theorem HCPolySupport.HighContrast.Multiscale.adapted_le_euclidean_comparison (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ) (C : ℝ), 0 < Csrc ∧ 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (t : ℤ), ↑jStar ≤ t → adaptedCell (Geometry.explicitRoundedGrid jStar m) t ⊆ centeredCube d (2 * ↑jStar) → ∀ (ℓ r : ℕ), 1 ≤ ℓ → 1 ≤ r → BlockMatLoewnerLE (blockSub (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (t + ↑ℓ + ↑r)) (blockScale (C * aspectRatio E * (‖m‖ * ‖m⁻¹‖) * 3 ^ (-↑r)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) t))) (adaptedMean P 1 (t + ↑ℓ))

E2 kernel: adapted-by-Euclidean comparison (HC's e.tilt.by.Euc, at the rounded grid; p.response.transfer, second inequality): for ℓ, r ≥ 1, 𝐀hom_{t+ℓ+r,q} ≤ 𝐀hom_{t+ℓ,Id} + C Π ‖m‖‖m⁻¹‖ 3^{-r} 𝐀hom_{t,q}. Same route with the roles exchanged: tile ⋄^q_{t+ℓ+r} by standard cells capped at t+ℓ. Use stationarity on the cap and the annealed source bound on every lower row, whose volume fraction is ≤ 12 d^{3/2} 3^{j-(t+ℓ+r)}. Normalize at the original generation t. The argument applies at every later generation without enlarging the source window. The stated unit-range assumption is again unnecessary.

Response inputs — support lemmas for K1 adapted_response_kernel and K2

persistence_transfer_kernel

Decomposition of the K1 adapted_response_kernel and K2 persistence_transfer_kernel inputs of the response transfer (Step 3 and Step 4). This file holds the non-kernel support lemmas; the analytic kernels are in HCPoly/Entry/Response/Core/EccentricityScaleDecay.lean.

Notation. q := Geometry.explicitRoundedGrid jStar m is the rounded grid (near e.rounded.grid.bounds), 𝐀hom_{j,q} := adaptedMean P q j, 𝐑 := blockSwap d, and 𝐑A⁻¹𝐑 is written out as in adaptedMean_swapConj_le. The canonical imbalance is 𝔡(A) = ‖G^{-1/2} A G^{-1/2}‖ with G = 𝐑A⁻¹𝐑 (canonicalImbalance), so 𝔡(A) ≤ c is the Loewner bound A ≤ c 𝐑A⁻¹𝐑.

Part P: adapted persistence (p.response.transfer, right half)

theorem HCPolySupport.HighContrast.Multiscale.loewner_swapConj_of_canonicalImbalance_le {d : ℕ} (_hd : 2 ≤ d) (A : BlockMat d) (hAs : IsSymmetricBlockMat A) (hA : Book.Ch02.BlockPosDef A) {c : ℝ} (hc : canonicalImbalance A ≤ c) : BlockMatLoewnerLE A (blockScale c (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat A)⁻¹ * toFullBlockMat (blockSwap d))))

P1. 𝔡(A) ≤ c unpacks to A ≤ c·𝐑A⁻¹𝐑. canonicalImbalance A is the operator norm of G^{-1/2} A G^{-1/2} with G = 𝐑A⁻¹𝐑 positive definite (near e.scale.selection.projective.distance); a symmetric positive semidefinite matrix with operator norm ≤ c is ≤ c·I, and conjugating back by G^{1/2} gives the claim. Mirror the route inside canonical_comparison_kernel (K3) and use sqrt_form, psd_dot_le_opNorm, swapConj_posDef from the helpers.

theorem HCPolySupport.HighContrast.Multiscale.swapConj_inv_antitone {d : ℕ} (X Y : BlockMat d) (hXs : IsSymmetricBlockMat X) (hX : Book.Ch02.BlockPosDef X) (hYs : IsSymmetricBlockMat Y) (hXY : BlockMatLoewnerLE X Y) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat Y)⁻¹ * toFullBlockMat (blockSwap d))) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat X)⁻¹ * toFullBlockMat (blockSwap d)))

P2. Inverse-and-swap reverses the Loewner order: for symmetric 0 < X ≤ Y, 𝐑Y⁻¹𝐑 ≤ 𝐑X⁻¹𝐑. inv_le_inv_of_le (helpers) gives Y⁻¹ ≤ X⁻¹; congruence by the symmetric involution 𝐑 (toFullBlockMat_blockSwap_mul_self) preserves the order.

theorem HCPolySupport.HighContrast.Multiscale.adaptedMean_persistence (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (t u : ℤ) (ht : ↑jStar ≤ t) (htu : t ≤ u) {δad : ℝ} (hδ : 0 ≤ δad) (himb : canonicalImbalance (adaptedMean P (Geometry.explicitRoundedGrid jStar m) t) ≤ 1 + δad) : BlockMatLoewnerLE (blockScale ((1 + δad) ^ (-↑d)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) t)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) u)

P3 persistence (p.response.transfer, right half; expanded manuscript hcp.e.random.persistence.transfer.adapted.persistence). For u ≥ t ≥ j_* and 𝔡(𝐀hom_{t,q}) ≤ 1 + δad: (1+δad)^{-d} 𝐀hom_{t,q} ≤ 𝐀hom_{u,q}. Route (stronger than the paper's determinant route, same conclusion): 𝐀_u ≤ 𝐀_t (adaptedMean_antitone); 𝐀_t ≤ (1+δad) 𝐑𝐀_t⁻¹𝐑 (P1) ≤ (1+δad) 𝐑𝐀_u⁻¹𝐑 (P2) ≤ (1+δad) 𝐀_u (adaptedMean_swapConj_le at u); finally (1+δad)^{-d} ≤ (1+δad)^{-1} and blockScale_loewner_mono (positivity from adaptedMean_posDef, symmetry from isSymmetricBlockMat_annealedBlock).

Part A: Loewner arithmetic and the gap choice (p.response.transfer)

theorem HCPolySupport.HighContrast.Multiscale.loewner_scale_sub_of_le {d : ℕ} (X Y A : BlockMat d) {a c : ℝ} (h1 : BlockMatLoewnerLE (blockSub X (blockScale c A)) Y) (h2 : BlockMatLoewnerLE (blockScale a A) X) : BlockMatLoewnerLE (blockScale (a - c) A) Y

A4 (Loewner arithmetic). From X - c·A ≤ Y and a·A ≤ X follows (a - c)·A ≤ Y (the lower bound: combine the reverse comparison with persistence at m_ent + r). Unfold BlockMatLoewnerLE; blockSub/blockScale are entrywise, so the quadratic forms are linear.

theorem HCPolySupport.HighContrast.Multiscale.exists_gap_of_eccentricity (C Cglob η : ℝ) (hC : 0 < C) (hCglob : 0 < Cglob) (hη : η ∈ Set.Ioo 0 1) : ∃ (Cresp : ℝ), 0 < Cresp ∧ ∀ (Pival e : ℝ), 1 ≤ Pival → 1 ≤ e → e ^ (1 / 2) ≤ (2 + Pival) ^ Cglob → ∃ (ℓ : ℕ), 1 ≤ ℓ ∧ C * Pival * e * 3 ^ (-↑ℓ) ≤ η ∧ ↑ℓ ≤ Cresp * Real.logb 3 (2 + Pival)

A2 (real analysis). The gap choice: with the source constant C = C(d,γ), the eccentricity exponent Cglob and a target η, there is Cresp such that for every Pival ≥ 1 and e = ‖m‖‖m⁻¹‖ ≥ 1 with e^{1/2} ≤ (2+Pival)^{Cglob} (RawOutput ecc) some ℓ ≥ 1 has C Pival e 3^{-ℓ} ≤ η and ℓ ≤ Cresp log₃(2+Pival). Take ℓ := ⌈log₃(C Pival e / η)⌉₊ + 1; then ℓ ≤ 2 + log₃ C + (1 + 2 Cglob) log₃(2+Pival) + log₃(1/η) and log₃(2+Pival) ≥ 1 since 2 + Pival ≥ 3.

Part S: the printed Step-3 bookkeeping (p.response.transfer)

theorem HCPolySupport.HighContrast.Multiscale.scale_decay_of_hs_lo (jStar : ℕ) (s : ℤ) (B Pival ρ : ℝ) (hPival : 3 ≤ 2 + Pival) (hρ : 0 ≤ ρ) (hs : ↑jStar + ⌈B * Real.logb 3 (2 + Pival)⌉ ≤ s) : 3 ^ (-(ρ * (↑s - ↑jStar))) ≤ (2 + Pival) ^ (-(ρ * B))

S1. e.global.selection.scales (RawOutput hs_lo, j_* + ⌈B log₃(2+Pival)⌉ ≤ s) turns 3^{-ρ(s - j_*)} into (2+Pival)^{-ρB} for ρ ≥ 0.

theorem HCPolySupport.HighContrast.Multiscale.exists_Bresp_of_decay (C Cglob ρ τ : ℝ) (hC : 0 < C) (hCglob : 0 < Cglob) (hρ : 0 < ρ) (hτ : 0 < τ) : ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∀ (B Pival : ℝ), Bresp ≤ B → 3 ≤ 2 + Pival → C * (2 + Pival) ^ (1 + 2 * Cglob - ρ * B) ≤ τ

S2. Since 2 + Pival ≥ 3 and the exponent 1 + 2 Cglob does not depend on B, choosing Bresp after σ makes C (2+Pival)^{1 + 2 Cglob - ρ B} ≤ τ for every B ≥ Bresp.