High-contrast homogenization: Annealed.Measurability

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

Measurability of the coarse response over the coefficient space

Every entry of the variational coarse block 𝐀(□_m; ·) of s.introduction is measurable for the canonical measurable structure of the coefficient space, which is the global sigma-field F = F(ℝ^d) generated by the smooth linear statistics. Measurability is therefore a fact about the coefficient space alone: it holds for every law at once, and the well-formedness predicate HasMeasurableCoarseBlock that e.Theta.m presupposes never has to be assumed.

The entries reduce to the variational quantity Mu at the four doubled vectors built from a pair of basis directions, so the whole statement is the measurability of a ↦ Mu (□_m) Q a. That is obtained by transporting the coarse-grained energy along a representative map into CoarseGraining's exact coarse-source carrier, whose own local sigma-fields are generated by exactly the same bilinear test integrals: the representative map pulls the generators back to the generators, and Mu only sees the almost everywhere class of the field, so the value is unchanged.

A representative in the exact coarse-source carrier

theorem HCPolySupport.HighContrast.exists_sourceCarrier_ae_eq {d : ℕ} (a : CoeffSpace d) : ∃ (b : Source.Coarse.Carrier d), ↑↑a =ᵐ[MeasureTheory.volume] ↑b

Every point of the coefficient space is represented, up to a null set, by a field of the exact coarse-source carrier: a measurable field that is uniformly elliptic on every ball with reciprocal constants. The sample's ellipticity constants on that ball supply the reciprocal constant, once normalized to lie in (0, 1].

noncomputable def HCPolySupport.HighContrast.sourceRepresentative {d : ℕ} (a : CoeffSpace d) : Source.Coarse.Carrier d

The chosen coarse-source representative of a point of the coefficient space.

Equations

• HCPolySupport.HighContrast.sourceRepresentative a = ⋯.choose

theorem HCPolySupport.HighContrast.sourceRepresentative_ae_eq {d : ℕ} (a : CoeffSpace d) : ↑↑a =ᵐ[MeasureTheory.volume] ↑(sourceRepresentative a)

The coarse-source representative carries the sample's field.

theorem HCPolySupport.HighContrast.bilinearTest_sourceRepresentative {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffSpace d) : Source.Coarse.bilinearTest e e' φ (sourceRepresentative a) = coeffPairing e e' φ a

The bilinear test integrals of the coarse-source carrier pull back along the representative map to the generating linear statistics of F(U): both are the same integral, and the two integrands agree almost everywhere.

theorem HCPolySupport.HighContrast.measurable_sourceRepresentative {d : ℕ} : Measurable sourceRepresentative

The representative map is measurable for the global sigma-fields: it pulls each generator of the coarse-source carrier back to a generator of F(ℝ^d), the test functions of the two families being the same.

The variational quantity is measurable

theorem HCPolySupport.HighContrast.Mu_centeredCube_eq_Mu_cubeSet {d : ℕ} (m : ℤ) (Q : BlockVec d) (f : CoeffField d) : Mu (centeredCube d m) Q f = Mu (cubeSet (originCube d m)) Q f

The variational quantity does not distinguish the open realization □_m of the centered triadic cube from the half-open realization used internally.

theorem HCPolySupport.HighContrast.measurable_Mu_centeredCube {d : ℕ} (m : ℤ) (Q : BlockVec d) : Measurable fun (a : CoeffSpace d) => Mu (centeredCube d m) Q ↑↑a

The coarse-grained energy of a centered cube is measurable on the coefficient space, for the global sigma-field F(ℝ^d). The coarse-source energy is local for the bilinear test sigma-field of the cube, hence measurable for the global one, and the representative map is measurable and leaves the energy unchanged.

The coarse response is measurable

theorem HCPolySupport.HighContrast.measurable_blockMatEntry_coarseBlock {d : ℕ} (m : ℤ) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock (centeredCube d m) a) α β

Every entry of the coarse block response on a centered cube is measurable for the canonical measurable structure of the coefficient space: the entries are the variational quantities at the four doubled vectors built from a pair of basis directions.

theorem HCPolySupport.HighContrast.hasMeasurableCoarseBlock_centeredCube {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m : ℤ) : HasMeasurableCoarseBlock P (centeredCube d m)

The coarse response is measurable over every law: the well-formedness predicate that e.Theta.m presupposes is a theorem of the coefficient space, not an assumption on the law.