High-contrast homogenization: Entry.Annealed.AdaptedDomainLocality

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

The adapted cell's domain and its local σ-fields

Recovery of the adapted cell as a domain of the coarse block, and the local independence of the coefficient field over separated cells that the annealed estimates are read in. On the actual qualitative carrier, boundedness supplies a pointwise elliptic representative of each field on the cell, giving strict positive definiteness of its coarse block and the mixed response formula; the support-generated σ-fields of unit-separated cells are independent under a unit-range law. The module serves the parent--child recurrence p.fixed.geometry.parent.child.recurrence.

Coefficient-carrier boundary for adapted-domain recovery support

This file transports strict positivity and the mixed response formula from CG affine open cubes to the qualitative coefficient carrier. Boundedness supplies each field's ellipticity constants on the cell; a.e. congruence returns both observables to its original representative. The endpoints assume no law-integrability or law-uniform ellipticity bound.

Source: near e.scale.selection.normalized.mean.fluctuation, p.fixed.geometry.parent.child.recurrence; the pathwise block structure comes from HC. Annealed positivity still requires the separate law-integrability input to the existing expectation theorem.

theorem HCPolySupport.HighContrast.Annealed.adaptedCellTranslate_eq_cg_affine {d : ℕ} (q : Mat d) (j : ℤ) (y : Vec d) : adaptedCellTranslate q j y = translateSet y (matVecMul q '' openCubeSet (originCube d j))

theorem HCPolySupport.HighContrast.Annealed.exists_elliptic_representative_adapted {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffSpace d) : ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticFieldOn lam Lam (adaptedCellTranslate q j y) f ∧ ↑↑a =ᵐ[MeasureTheory.volume] f

Boundedness supplies a pointwise elliptic representative of each qualitative field on the cell. The constants depend only on this field and region and remain internal to the pathwise proof.

theorem HCPolySupport.HighContrast.Annealed.blockPosDef_coarseBlock_adapted {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffSpace d) : Book.Ch02.BlockPosDef (coarseBlock (adaptedCellTranslate q j y) a)

Pathwise strict positivity on the actual qualitative coefficient carrier.

theorem HCPolySupport.HighContrast.Annealed.responseJ_eq_coarseBlock_adapted {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffSpace d) (p r : Vec d) : ResponseJ (adaptedCellTranslate q j y) p r ↑↑a = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (coarseBlock (adaptedCellTranslate q j y) a) (-p, r)) - vecDot p r

The mixed response formula for the coefficient representative and coarse block.

Local independence on the coefficient sigma-fields

This file works directly with the carrier CoeffSpace and the support-generated sigma-fields coeffSigma. It deliberately does not coerce the law to an AKL fixed-ellipticity carrier.

theorem HCPolySupport.HighContrast.Annealed.coeffSigma_le_global {d : ℕ} (U : Set (Vec d)) : coeffSigma d U ≤ inferInstance

theorem HCPolySupport.HighContrast.Annealed.measurable_coeffPairing_local {d : ℕ} {U : Set (Vec d)} (e e' : Vec d) {φ : Vec d → ℝ} (hφ : IsLocalTest U φ) : Measurable (coeffPairing e e' φ)

theorem HCPolySupport.HighContrast.Annealed.iIndep_coeffSigma_of_isUnitRangeLaw {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) (U : ι → Set (Vec d)) (hU : ∀ (i : ι), MeasurableSet (U i)) (hsep : Pairwise fun (i j : ι) => UnitSeparated (U i) (U j)) : ProbabilityTheory.iIndep (fun (i : ι) => coeffSigma d (U i)) P

theorem HCPolySupport.HighContrast.Annealed.iIndepFun_of_coeffSigma_measurable {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) (U : ι → Set (Vec d)) (hU : ∀ (i : ι), MeasurableSet (U i)) {β : ι → Type u_2} [(i : ι) → MeasurableSpace (β i)] (X : (i : ι) → CoeffSpace d → β i) (hX : ∀ (i : ι), Measurable (X i)) (hsep : Pairwise fun (i j : ι) => UnitSeparated (U i) (U j)) : ProbabilityTheory.iIndepFun X P