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

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

The pathwise fluctuation bound

This file proves the pathwise bound on the normalized fluctuation of the response block across scales, the all-scale estimate serving p.response.transfer: it identifies the normalized fluctuation with an explicit difference of normalized blocks, bounds a single fluctuation term by the operator norm through the Loewner order, and controls the resulting geometric sum by the elementary inequality (1 + 3^{-k})^n ≤ 3 on a compatible range. It also proves the monotonicity of the block scale and the bound on the spectral bound of a single cell, which the pathwise estimate needs at each scale.

theorem HCPolySupport.HighContrast.Multiscale.profile_self_le_eta (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (ε σ 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) (η : ℝ) (hprof : Cprof * σ ^ ((1 - γ) / 8) ≤ η) : profile P γ (respGrid jStar F) jStar t t ≤ η

The complete profile at the top of the response window is at most eta (p.response.transfer, "decreasing sigma_0 makes every profile and drift in e.global.selection.profile at most eta"). raw.prof bounds the sum of the three profiles and the two drifts; the two drifts are nonnegative (Multiscale.determinantDrift_nonneg), so the top profile alone is below C_prof sigma^{(1-gamma)/8}, which hprof puts below eta.

helpers

The helpers supplying the source branch k < j_* of the all-scale maximum, together with the three block-algebra facts it needs: the Loewner envelope of an arbitrary (not positive semidefinite) doubled block by its operator norm, the attainment of the infimum defining blockSpecBound, and the normalization of a Loewner bound A <= c R by the positive definite R itself.

theorem HCPolySupport.HighContrast.Multiscale.loewner_le_blockOpNorm_general {d : ℕ} (N : BlockMat d) : BlockMatLoewnerLE N (blockScale (blockOpNorm N) (Book.Ch02.blockIdentity d))

The Loewner envelope of an arbitrary doubled block by its operator norm.

theorem HCPolySupport.HighContrast.Multiscale.normalizedBlock_le_scale {d : ℕ} (A R : BlockMat d) (hR : Matrix.PosDef (toFullBlockMat R)) (c : ℝ) (h : BlockMatLoewnerLE A (blockScale c R)) : BlockMatLoewnerLE (normalizedBlock A R) (blockScale c (Book.Ch02.blockIdentity d))

Normalizing a Loewner bound A ≤ c R by the positive definite R itself.

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

The quadratic form is homogeneous in a scalar dilation.

theorem HCPolySupport.HighContrast.Multiscale.blockScale_mono_of_nonneg {d : ℕ} (A R : BlockMat d) (c k : ℝ) (hc : 0 ≤ c) (h : BlockMatLoewnerLE A (blockScale k R)) : BlockMatLoewnerLE (blockScale c A) (blockScale (c * k) R)

A scalar dilation of a Loewner bound.

theorem HCPolySupport.HighContrast.Multiscale.blockSpecBound_attained_of_loewnerLE {d : ℕ} (N : BlockMat d) (c : ℝ) (hc : 0 ≤ c) (h : BlockMatLoewnerLE N (blockScale c (Book.Ch02.blockIdentity d))) : BlockMatLoewnerLE N (blockScale (blockSpecBound N) (Book.Ch02.blockIdentity d))

The infimum defining blockSpecBound is attained when the defining set is nonempty.

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

The crude three-term power inequality.

theorem HCPolySupport.HighContrast.Multiscale.pow_weight (ρ : ℝ) (n Q : ℕ) (x : ℝ) : (3 ^ (-(ρ * ↑n)) * x) ^ Q = 3 ^ (-↑Q * ρ * ↑n) * x ^ Q

The Q-th power of a weighted quantity.

theorem HCPolySupport.HighContrast.Multiscale.le_rpow_inv (Q : ℕ) (hQ : Q ≠ 0) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x ^ Q ≤ y) : x ≤ y ^ (↑Q)⁻¹

Passing to the Q-th root of a bound.

theorem HCPolySupport.HighContrast.Multiscale.adaptedCellTranslate_center {d : ℕ} (q : Mat d) (j : ℤ) (z : Fin d → ℤ) : adaptedCellTranslate q j (adaptedCellCenter q j z) = adaptedCellAtCenter q j z

The aligned adapted cell is the translate of the adapted cell to its centre.

theorem HCPolySupport.HighContrast.Multiscale.normalizedFluctuation_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (j k : ℤ) (z : Fin d → ℤ) (a : CoeffSpace d) : normalizedFluctuation P q j k (adaptedCellCenter q j z) a = normalizedBlock (blockSub (coarseBlock (adaptedCellAtCenter q j z) a) (adaptedMean P q j)) (adaptedMean P q k)

The normalized fluctuation at an aligned centre, spelled with adaptedCellAtCenter.

theorem HCPolySupport.HighContrast.Multiscale.pathwise_bound_max (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (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 γ))) : respAllScaleMax 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

The pathwise all-scale bound: the two branches combined through respAllScaleMax_le_of_forall.