AveragedChain

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the averaged block chain e.CG.bounds.2

This file proves a local version of the right-hand inequality of the display e.CG.bounds.2 in ABK26,

(⨍_U bfA⁻¹(x) dx)⁻¹ ≤ bfA_*(U) ≤ bfA(U) ≤ ⨍_U bfA(x) dx,

for an admissible block coefficient field on a Chapter 2 domain, in the doubled Loewner order Homogenization.BlockMatLoewnerLE.

The inequality is proved by the variational route of the notes, and is accompanied by the order isomorphism that turns it into the left-hand bound.

• Right, bfA(U) ≤ ⨍_U bfA. The constant doubled field x ↦ P is admissible for the doubled mu problem at load P (its fluctuation is zero), so the minimum mu(U,P) is at most the energy of that competitor, which is ½ P ⬝ (⨍_U bfA) P by average_blockEnergyDensityAt. On the other side Book.Ch02.DoubledMuTheory.mu_quadratic identifies mu(U,P) = ½ P ⬝ bfA(U) P.

• Reflection. In the doubled formalism the pointwise inverse is the block reflection, bfA⁻¹(x) = blockReflect (bfA(x)), exactly as bfA_*⁻¹(U) = blockReflect (bfA(U)) at the coarse level. Reflection is an order isomorphism for the doubled Loewner order (blockMatLoewnerLE_blockReflect), so the dual form of the left-hand bound — bfA_*⁻¹(U) ≤ ⨍_U bfA⁻¹(x) dx, the form that does not invert a matrix — is the block reflection of the right-hand bound.

Right inequality: bfA(U) ≤ ⨍_U bfA(x) dx

theorem Algsuperdiff.Section3.Provider.Block.isDoubledMuAdmissible_const {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (P : HCPolySupport.BlockVec d) : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U P { potential := fun (x : HCPolySupport.Vec d) => P.1, flux := fun (x : HCPolySupport.Vec d) => P.2 }

The constant doubled field at load P is admissible for the doubled mu problem at load P: its fluctuation vanishes identically.

theorem Algsuperdiff.Section3.Provider.Block.coarseBlockMatrix_blockMatLoewnerLE_averagedBlockMatrix {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.BlockMatLoewnerLE (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (averagedBlockMatrix U a)

e.CG.bounds.2, right inequality: the coarse block matrix is dominated by the volume average of the pointwise doubled coefficient matrix.