High-contrast homogenization: Entry.Annealed.AveragingTransport

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

Integrability, lattice centering, and stationarity transport

For the cell q = Geometry.explicitRoundedGrid jStar m, deterministic centre A, conjugator R and Y y = fun a => normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate q j y) a) A) R, the normalized recentred block Y y lies in L^N(S_N) for every real N ≥ 1, every generation j and every centre y, with no membership premise beyond the standing law; at a lattice centre adaptedCellCenter q j w of generation j_* ≤ j its entrywise mean vanishes; and the lattice translation that moves the centre to the origin leaves its block-valued mixed norm unchanged, ‖Y z‖_{L^N(S_N)} = ‖Y 0‖_{L^N(S_N)}, with A and R held fixed. These centering, moment and stationarity facts serve the finite-range matrix averaging lemma l.fixed.geometry.matrix.averaging and the mean and profile estimates of the two-grid transport p.two.grid.transport.

The cell at the origin

theorem HCPolySupport.HighContrast.Annealed.adaptedCellTranslate_zero {d : ℕ} (q : Mat d) (j : ℤ) : adaptedCellTranslate q j 0 = adaptedCell q j

adaptedCellTranslate q j 0 = adaptedCell q j. The right-hand side is the untranslated cell; the lattice picture writes it as the translate by 0.

Integrability receipts

theorem HCPolySupport.HighContrast.Annealed.memLqSchatten_normalizedCentered (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 : ℕ) (hjS : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (y : Vec d) (R : BlockMat d) (N : ℝ) (hN : 1 ≤ N) : SchattenMemLp P N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R

The integrability receipt. Y y lies in L^N(S_N) for every real N ≥ 1, every generation j and every centre y. No membership premise is added to any statement; this is derived from the standing law.

theorem HCPolySupport.HighContrast.Annealed.memLqSchatten_normalizedCentered_sum (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 : ℕ) (hjS : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (R : BlockMat d) (N : ℝ) (hN : 1 ≤ N) {ι : Type u_1} (s : Finset ι) (w : ι → ℝ) (y : ι → Vec d) : SchattenMemLp P N fun (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ s, w i • toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j (y i)) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R))

The full normalized average lies in L^N(S_N) as well, through memLqSchatten_finset_sum in the shape the class average uses.

Centering at a lattice cell

theorem HCPolySupport.HighContrast.Annealed.annealedBlock_adaptedCellTranslate_lattice {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (hjS : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) : annealedBlock P (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) j w)) = adaptedMean P (Geometry.explicitRoundedGrid jStar m) j

The annealed block of a cell centred at a lattice point of the same generation is the adapted mean. annealedBlock_adaptedCellAtCenter, moved to the adaptedCellTranslate picture.

theorem HCPolySupport.HighContrast.Annealed.integral_normalizedCentered_lattice_eq_zero {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 : ℕ) (hjS : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) (R : BlockMat d) : ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) j w)) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R) α β ∂P) = ofFullBlockMat 0

Centering. For a cell centred at a lattice point of generation j ≥ j_* the entrywise mean of Y z vanishes. This is the hcent premise, in the Matrix.of fun α β => ∫ … shape that premise uses; the same object is stated as fun α β => ∫ …, and the two are bridged here rather than left to coincide.

Stationarity transport of the block-valued mixed norm

theorem HCPolySupport.HighContrast.Annealed.normalizedCentered_lattice_eq_comp_translateCoeff {d : ℕ} (jStar : ℕ) (m : Mat d) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) (A R : BlockMat d) : ∃ (v : Fin d → ℤ), (fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) j w)) a) A) R) = (fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) A) R) ∘ translateCoeff v

The block at a lattice-centred cell is the block at the origin precomposed with the integer translation of the coefficient field. A and R are deterministic and do not move.

theorem HCPolySupport.HighContrast.Annealed.lqSchattenNorm_normalizedCentered_transport {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (m : Mat d) {j : ℤ} (hj : ↑jStar ≤ j) (w : Fin d → ℤ) (A R : BlockMat d) {N : ℝ} (hN : 1 ≤ N) (hmem : SchattenMemLp P N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) A) R) : (lqSchattenNorm P N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) j w)) a) A) R) = lqSchattenNorm P N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) A) R

Stationarity transport. ‖Y z‖_{L^N(S_N)} = ‖Y 0‖_{L^N(S_N)} for every lattice centre z = adaptedCellCenter q j w with j_* ≤ j.

Route: adaptedCellCenter_eq_intTranslation writes the centre as an integer translation; coarseBlock_adapted_translateCoeff turns the shifted cell into a precomposition with translateCoeff v; IsStationaryLaw says Measure.map (translateCoeff v) P = P; and the scalar integrand is AEStronglyMeasurable, so the change of variables for the Bochner integral applies. This is the block-valued transport, at the block level rather than merely entrywise.