AveragedBlock

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

Provider: the volume-averaged doubled coefficient matrix

The chain e.CG.bounds.2 in ABK26,

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

compares the coarse block matrices with volume averages of the pointwise doubled coefficient field. CoarseGraining names the pointwise field Homogenization.Book.Ch02.blockMatrixField and its pointwise inverse Homogenization.Book.Ch02.blockMatrixInverseField, but has no averaged block matrix; this file introduces them, following the averageMat conventions of Homogenization/Book/Ch02/Matrices.lean.

The analytic content of the file is the exchange of the volume average with the doubled quadratic form,

⨍_U X ⬝ bfA(x) X dx = X ⬝ (⨍_U bfA(x) dx) X,

which needs integrability of the 2d × 2d entries of bfA(x) on U. That is discharged entirely from the CoeffOn carrier: CoeffOn.aeElliptic gives a.e. ellipticity of the representative on U, which bounds every doubled entry by Real.sqrt (blockMatrixOfCoeffNormSqBound lam Lam), and the pointwise-good representative Internal.Ch02.BookCh02.pointwiseCoeffOn supplies a genuinely measurable coefficient field a.e. equal to a, whence a.e. strong measurability of the doubled entries. Chapter 2 domains carry finite volume, so bounded plus a.e. strongly measurable is integrable.

The averaged doubled coefficient matrices

noncomputable def Algsuperdiff.Section3.Provider.Block.averagedBlockMatrix {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.BlockMat d

The volume average ⨍_U bfA(x) dx of the pointwise doubled coefficient field over a Chapter 2 domain.

Equations

• One or more equations did not get rendered due to their size.

The pointwise inverse field really is the pointwise inverse

blockMatrixInverseField is defined as an explicit block formula, so its name alone does not certify that it inverts blockMatrixField. The two lemmas below record the genuine two-sided identification, a.e. on the Chapter 2 domain, from CoeffOn.aeElliptic and CoarseGraining's pointwise block Fenchel inverse identity Homogenization.blockMatMul_blockReflect_blockMatrixOfCoeff_eq_id. They document the left-hand term ⨍_U bfA⁻¹(x) dx of e.CG.bounds.2 as the average of the genuine pointwise inverse.

theorem Algsuperdiff.Section3.Provider.Block.toFullBlockMat_averagedBlockMatrix {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (alpha beta : HCPolySupport.BlockCoord d) : HCPolySupport.toFullBlockMat (averagedBlockMatrix U a) alpha beta = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockMatrixField a x) alpha beta

Entries of the averaged doubled matrix are the averages of the entries.

The doubled quadratic form as a sum over doubled coordinates

theorem Algsuperdiff.Section3.Provider.Block.blockVecDot_blockMatVecMul_eq_sum {d : ℕ} (A : HCPolySupport.BlockMat d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul A X) = ∑ alpha : HCPolySupport.BlockCoord d, ∑ beta : HCPolySupport.BlockCoord d, HCPolySupport.toFullBlockVec X alpha * HCPolySupport.toFullBlockMat A alpha beta * HCPolySupport.toFullBlockVec X beta

The doubled quadratic form written out over the 2d doubled coordinates.

Integrability of the doubled entries

theorem Algsuperdiff.Section3.Provider.Block.integrable_toFullBlockMat_blockMatrixField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (alpha beta : HCPolySupport.BlockCoord d) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockMatrixField a x) alpha beta) (HCPolySupport.volumeMeasureOn U.carrier)

Every entry of the pointwise doubled coefficient matrix is integrable on a Chapter 2 domain.

Measurability comes from the pointwise-good representative Internal.Ch02.BookCh02.pointwiseCoeffOn, whose coefficient field is genuinely measurable and a.e. equal to a; the bound comes from CoeffOn.aeElliptic.

Linearity of the normalized average

theorem Algsuperdiff.Section3.Provider.Block.average_const_mul {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (c : ℝ) (f : HCPolySupport.Vec d → ℝ) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => c * f x) = c * HCPolySupport.Book.Ch02.average U f

The normalized average is homogeneous.

The average commutes with the doubled quadratic form

theorem Algsuperdiff.Section3.Provider.Block.average_blockVecDot_blockMatVecMul_blockMatrixField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) X)) = HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (averagedBlockMatrix U a) X)

Exchanging the volume average with the doubled quadratic form: the average of the pointwise doubled energy is the doubled energy of the averaged matrix.

theorem Algsuperdiff.Section3.Provider.Block.average_blockEnergyDensityAt {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt a X x) = 1 / 2 * HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (averagedBlockMatrix U a) X)

The average over U of the pointwise doubled energy density at a fixed doubled load is the doubled energy of the averaged matrix.

theorem Algsuperdiff.Section3.Provider.Block.integrable_blockVecDot_blockMatVecMul_blockMatrixField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) X)) (HCPolySupport.volumeMeasureOn U.carrier)

The pointwise doubled energy at a fixed load is integrable on U.