High-contrast homogenization: Entry.Annealed.AdaptedCellFoundations

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

Integrability on the adapted cell and the aligned subdivision

Integrability of the coarse block on an adapted cell, and the combinatorics of the aligned triadic subdivision the annealed estimates are carried out over. The module establishes law integrability of every entry of an actual adapted coarse block and full positive definiteness of the adapted annealed means, then describes the finite aligned subdivision of a parent adapted cell into its triadic descendants, their centers, disjointness and common relative volume. It serves the parent-child recurrence p.fixed.geometry.parent.child.recurrence.

Finite positive adapted expectations

The actual law integrability uses arbitrary finite moments, with an auxiliary bounded window. No original-window containment or fixed-Q source threshold is needed for ordinary support lemmas. Source-facing consumers retain the source lower scale.

theorem HCPolySupport.HighContrast.Annealed.hasIntegrableCoarseBlock_adapted (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) (j : ℤ) (y : Vec d) : HasIntegrableCoarseBlock P (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y)

Every entry of an actual adapted coarse block is law integrable.

theorem HCPolySupport.HighContrast.Annealed.adaptedMean_posDef (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) (j : ℤ) : Matrix.PosDef (toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j))

Full positive definiteness of the actual adapted annealed means, at every integer generation, from the standing stationary dagger law.

Finite aligned subdivisions

These are the actual triadic descendants used at p.fixed.geometry.parent.child.recurrence. The integer translation assertion retains the lower alignment threshold jStar ≤ j.

theorem HCPolySupport.HighContrast.Annealed.alignedCenter_mem_iff (d : ℕ) (j : ℤ) (h : ℕ) (w : Fin d → ℤ) (b : ℕ) (hb : 3 ^ h = 2 * b + 1) : standardCellCenter j w ∈ centeredCube d (j + ↑h) ↔ ∀ (i : Fin d), -↑b ≤ w i ∧ w i ≤ ↑b

An aligned center belongs to its parent precisely on the finite integer box.

theorem HCPolySupport.HighContrast.Annealed.alignedCenterSet_finite_card (d : ℕ) (j : ℤ) (h : ℕ) : {w : Fin d → ℤ | standardCellCenter j w ∈ centeredCube d (j + ↑h)}.Finite ∧ {w : Fin d → ℤ | standardCellCenter j w ∈ centeredCube d (j + ↑h)}.ncard = 3 ^ (d * h)

Every nonnegative gap gives exactly 3^(d*h) centers, including the singleton h=0.

theorem HCPolySupport.HighContrast.Annealed.adaptedCellCenter_eq_intTranslation {d : ℕ} (jStar : ℕ) (m : Mat d) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) : ∃ (z : Fin d → ℤ), adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) j w = Source.AKL.intTranslation z

Each actual rounded-grid center is an integer translation at admissible scales.

theorem HCPolySupport.HighContrast.Annealed.aligned_standard_partition {d : ℕ} (j : ℤ) (h : ℕ) : have s := {w : Fin d → ℤ | standardCellCenter j w ∈ centeredCube d (j + ↑h)}; (∀ w ∈ s, standardCell d j w ⊆ centeredCube d (j + ↑h)) ∧ s.PairwiseDisjoint (standardCell d j) ∧ MeasureTheory.volume (centeredCube d (j + ↑h) \ ⋃ w ∈ s, standardCell d j w) = 0

Standard cells at a fixed finer generation form the full finite parent partition.

theorem HCPolySupport.HighContrast.Annealed.aligned_adapted_partition {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (h : ℕ) : have s := {w : Fin d → ℤ | standardCellCenter j w ∈ centeredCube d (j + ↑h)}; (∀ w ∈ s, adaptedCellAtCenter q j w ⊆ adaptedCell q (j + ↑h)) ∧ s.PairwiseDisjoint (adaptedCellAtCenter q j) ∧ MeasureTheory.volume (adaptedCell q (j + ↑h) \ ⋃ w ∈ s, adaptedCellAtCenter q j w) = 0

The invertible affine image preserves the aligned partition and its null boundaries.

theorem HCPolySupport.HighContrast.Annealed.aligned_adapted_volume_ratio {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (h : ℕ) (w : Fin d → ℤ) : (MeasureTheory.volume (adaptedCellAtCenter q j w)).toReal / (MeasureTheory.volume (adaptedCell q (j + ↑h))).toReal = (3 ^ (d * h))⁻¹

Each child has the same relative volume 3^(-d*h) in the full adapted parent.