High-contrast homogenization: Entry.Response.Kernel.DepthZeroEnergyExtraction

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

The depth-zero extraction and measurability of the all-scale maximum

This file proves step (ii) of the energy-split argument, p.response.transfer: the coarse block at depth 0 is bounded by (1 + M) E_t, where M = respAllScaleMax is a supremum over a countable family that is almost-everywhere bounded above. It establishes the measurability and nonnegativity of respAllScaleMax needed to make that supremum well behaved, and the resulting depth-0 bound on the squared optimizer energy for both the recentred and adjoint coefficients.

Block E: step (ii) -- the depth-0 extraction.

Block F: the load normalization p · q^∓ = 1, copied from the sorry-free helpers of HCPoly/Entry/Response/Core/ResponseCalibrationBundles.lean — private vecDot_add_right_distrib, respSkew_isSkew_matTranspose, vecDot_respP_respQ_eq_vecDot_self and public vecDot_skew_self_of_matTranspose.

theorem HCPolySupport.HighContrast.Multiscale.weakOptimizerEnergy_sq_le_minus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (ε σ Cglob Cprof Csrc Bresp : ℝ) (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 → ∀ (e : Vec d), vecDot e e = 1 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffMinus F a) (respCell jStar F t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a) (u a)) → ∀ᵐ (a : CoeffSpace d) ∂P, weakOptimizerEnergy (respCell jStar F t) (respCoeffMinus F a) (u a) ^ 2 ≤ (1 + respAllScaleMax P γ jStar F t a) * respLsqMinus P jStar F t e

The pathwise optimizer energy is the quadratic form of the recentred coarse block, ℰ_t^2 = 2J_t = x^-·A^b_t(a)x^- (paper p.response.transfer), and the depth-0 term of M gives the one-sided bound A_t(a) ≤ (1 + M(a)) E_t (blockSpecBound, congruence by respG via coarseBlockMatrix_sub_skew_eq_blockCongr, Ehat = blockCongr respG E_t), so ℰ_t^2 ≤ (1 + M(a)) (L^-)^2. Only a.e. in a: the junk value sSup = 0 of an unbounded set must be excluded, and it is -- by coarseBlock_le_one_add_respAllScaleMax below, whose BddAbove comes from Source.bounded_source_envelope (HCPoly/Entry/Source/BoundedWindowFiniteness.lean) applied to the bounded window U_t, fed by raw.stat and raw.ell.

theorem HCPolySupport.HighContrast.Multiscale.weakOptimizerEnergy_sq_le_plus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (ε σ Cglob Cprof Csrc Bresp : ℝ) (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 → ∀ (e : Vec d), vecDot e e = 1 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (respCell jStar F t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a) (u a)) → ∀ᵐ (a : CoeffSpace d) ∂P, weakOptimizerEnergy (respCell jStar F t) (respCoeffPlus F a) (u a) ^ 2 ≤ (1 + respAllScaleMax P γ jStar F t a) * respLsqPlus P jStar F t e

The + counterpart of the preceding estimate.

theorem HCPolySupport.HighContrast.Multiscale.respAllScaleMax_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) : 0 ≤ respAllScaleMax P γ jStar F t a

0 ≤ M (Real.sSup_nonneg: every member is 3^{-ρn} · blockSpecBound ≥ 0, blockSpecBound is an sInf of {c | 0 ≤ c ∧ …}, junk 0).

theorem HCPolySupport.HighContrast.Multiscale.energy_split_pointwise (m E L θ : ℝ) (Q : ℕ) (hQ : 2 ≤ Q) (hL : 0 ≤ L) (hm : 0 ≤ m) (hE : E ^ 2 ≤ (1 + m) * L) : ((if 1 < m then √m else θ) * E) ^ 2 ≤ 2 * L * (m ^ Q + θ ^ 2)

Pure real arithmetic of the split (p.response.transfer): on {m > 1}, m·(1+m) ≤ 2m^2 ≤ 2m^Q; on {m ≤ 1}, θ^2(1+m) ≤ 2θ^2.

Local helpers.

M = respAllScaleMax is the supremum of the countable family indexed by the depth n : ℕ and the finite index box triadicIndexBox d n (HCPoly/Entry/Response/Core/ResponseBlockObjects.lean), so its measurability reduces, through Measurable.sSup (Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean), to the measurability of one member. One member is blockSpecBound of the recentred normalized coarse block, and the two ingredients are:

• blockSpecBound (HCPoly/Entry/Response/Core/ResponseBlockObjects.lean) is ell^1-Lipschitz in the flattened entries of its argument. Its defining set {c | 0 ≤ c ∧ H ≤ c I} is closed (an intersection of half-lines, one per test vector), nonempty (the crude entrywise bound quad_le_entryAbsSum) and bounded below, so IsClosed.csInf_mem makes the infimum ATTAINED — that is what upgrades the one-sided blockSpecBound_le_of_loewner of HCPoly/Entry/Response/Core/EnergyDefectBound.lean to the Lipschitz estimate blockSpecBound_le_add, hence to continuity, hence to measurability. No positive semidefiniteness and no symmetry of the argument is needed, which is what makes this usable on the RECENTRED block normalizedBlock A E - I (the mine's route through the operator norm, HCPoly/Provider/Window/ScaleMeasurability.lean measurable_blockSize_coarseBlock via PortableHistory.blockSize_eq_norm, is only available on positive blocks).
• the entries of a ↦ coarseBlock (adaptedCellAtCenter q j w) a are measurable, by Annealed.measurable_coarseBlock_entry_adapted (HCPoly/Entry/Annealed/AdaptedLocality.lean) pushed to the global sigma-field by Annealed.coeffSigma_le_global; normalizedBlock is then a fixed bilinear expression in them.

The same shape is available for the POSITIVE carriers blockSize / blockExcess (HCPoly/Provider/Window/ScaleMeasurability.lean and HCPoly/Provider/Response/ProfileMaximumLp.lean, through aemeasurable_blockSize_adaptedResponse and the countable AEMeasurable.iSup over (k, w)), but there is no counterpart for the one-sided blockSpecBound of a recentred (indefinite) block, which is why the Lipschitz route below is written out here rather than reused.

def HCPolySupport.HighContrast.Multiscale.entryAbsSum {d : ℕ} (N : BlockMat d) : ℝ

The ell^1 size of the flattened entries of a doubled block.

Equations

• HCPolySupport.HighContrast.Multiscale.entryAbsSum N = ∑ α : HCPolySupport.BlockCoord d, ∑ β : HCPolySupport.BlockCoord d, |HCPolySupport.toFullBlockMat N α β|

theorem HCPolySupport.HighContrast.Multiscale.measurable_coarseBlock_entry {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) (w : Fin d → ℤ) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (coarseBlock (adaptedCellAtCenter q j w) a) α β

Every flattened entry of the coarse response on an aligned adapted cell is measurable for the global coefficient sigma-field.

theorem HCPolySupport.HighContrast.Multiscale.measurable_normalized_entry {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) (w : Fin d → ℤ) (E : BlockMat d) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter q j w) a) E) (Book.Ch02.blockIdentity d)) α β

The normalized recentred block of the coarse response is entrywise measurable.

theorem HCPolySupport.HighContrast.Multiscale.respAllScaleMax_measurable {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (hq : IsUnit (respGrid jStar F)) (t : ℤ) : Measurable (respAllScaleMax P γ jStar F t)

Measurability of M. M is the supremum of the countable family indexed by the depth n : ℕ and the finite index box triadicIndexBox d n, each member measurable through the coarse block of an aligned adapted cell.