High-contrast homogenization: Entry.Annealed.AdaptedLocality

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

Local measurability and covariance of adapted coarse blocks

The coarse block is recovered by polarization of CG's Mu. We adapt CG's Chapter 4 smooth-test route: approximate compact ball indicators by smooth cutoffs, prove measurable ellipticity slices, and realize the coefficient field in L² from the supported generating statistics. On each slice, Mu is the infimum of energies along a countable dense family of admissible corrections. The slice cover includes every coefficient field, giving strict local measurability without a law premise or a uniform ellipticity bound.

The helpers below extend the open-set part of CG's Probability/RegCoeffField/SmoothSliceMeasurability.lean and the countable variational argument of CoarseGraining/MuOperator/AEEOperator/CanonicalCubeSet.lean. The regular-carrier map and its sigma-algebra comparison are proved below. No adapted-domain recovery or identification with an AKL fixed-Θ law is used.

Source: near e.coarse.ellipticity, e.rounded.grid.bounds, e.fixed.geometry.parent.child; qualitative local ellipticity is assumed.

theorem HCPolySupport.HighContrast.Annealed.coarseBlock_adapted_translateCoeff {d : ℕ} (q : Mat d) (j : ℤ) (y : Vec d) (z : Fin d → ℤ) (a : CoeffSpace d) : coarseBlock (adaptedCellTranslate q j y) (translateCoeff z a) = coarseBlock (adaptedCellTranslate q j (y + Source.AKL.intTranslation z)) a

theorem HCPolySupport.HighContrast.Annealed.measurableSet_aeeSlice_of_entryTest_response {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {U : Set (Vec d)} (A : Ω → RegCoeffField d) (hU : IsOpen U) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, IsLocalTest U φ → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) (k : ℕ) : MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice U k (A ω).toFun}

Public slice-event measurability bridge used by the response optimizer-selection chain.

theorem HCPolySupport.HighContrast.Annealed.mu_eq_iInf_energy_for_responseSelection {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hvol : 0 < (MeasureTheory.volume U).toReal) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P0 : BlockVec d) : Mu U P0 ↑a = ⨅ (n : ℕ), blockEnergyAverage U (↑a) (canonicalMuGeneratorAffineField P0 (TopologicalSpace.denseSeq (↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) n))

Public general-cell countable-energy presentation used by the response measurable-selection chain. This exposes the already established Chapter-4 argument without adding any ellipticity constant to a downstream response statement.

theorem HCPolySupport.HighContrast.Annealed.measurable_coarseBlock_entry_adapted {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock (adaptedCellTranslate q j y) a) α β

Every entry of the coarse block on an invertible adapted cell is measurable for its support-local coefficient sigma algebra. The proof uses CG's countable variational infimum and proves the carrier comparison.

theorem HCPolySupport.HighContrast.Annealed.measurable_coarseBlock_matrix_adapted {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (coarseBlock (adaptedCellTranslate q j y) a)

The full unfolded matrix retains the same local sigma algebra.