High-contrast homogenization: Setup.ResponsePositivity

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

Positive definiteness of the coarse response on the coefficient space

Every field of the coefficient space is uniformly elliptic almost everywhere on every bounded set, so on each triadic cube it agrees almost everywhere with a measurable everywhere uniformly elliptic field, and the deterministic coarse-graining theory gives positive definiteness of the coarse response of that field. Since the coarse response only sees the almost everywhere class of the field on the cube, this is the sample-side half of the well-formedness that e.Theta.m presupposes.

def HCPolySupport.HighContrast.regCoeffFieldOfPointwiseElliptic {d : ℕ} {lam Lam : ℝ} (f : CoeffField d) (hfm : Measurable f) (hfp : ∀ (x : Vec d), IsEllipticMatrix lam Lam (f x)) : RegCoeffField d

A pointwise uniformly elliptic measurable field is a regular coefficient field: its entries are bounded by the upper ellipticity constant, hence locally integrable.

Equations

• HCPolySupport.HighContrast.regCoeffFieldOfPointwiseElliptic f hfm hfp = { toFun := f, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.regCoeffFieldOfPointwiseElliptic_toFun {d : ℕ} {lam Lam : ℝ} (f : CoeffField d) (hfm : Measurable f) (hfp : ∀ (x : Vec d), IsEllipticMatrix lam Lam (f x)) : (regCoeffFieldOfPointwiseElliptic f hfm hfp).toFun = f

theorem HCPolySupport.HighContrast.aeLocallyUniformlyEllipticField_of_pointwise {d : ℕ} {lam Lam : ℝ} {f : CoeffField d} (hfm : Measurable f) (hlam : 0 < lam) (hle : lam ≤ Lam) (hfp : ∀ (x : Vec d), IsEllipticMatrix lam Lam (f x)) : Book.Ch04.AELocallyUniformlyEllipticField (regCoeffFieldOfPointwiseElliptic f hfm hfp)

Pointwise uniform ellipticity gives locally uniform almost everywhere ellipticity, with the same constants on every triadic cube.

theorem HCPolySupport.HighContrast.locallyIntegrable_of_ball_bounded_measurable {d : ℕ} {f : Vec d → ℝ} (hf : Measurable f) (hbd : ∀ (R : ℝ), 0 < R → ∃ (C : ℝ), ∀ x ∈ Metric.ball 0 R, |f x| ≤ C) : MeasureTheory.LocallyIntegrable f MeasureTheory.volume

A measurable scalar field bounded on every ball around the origin is locally integrable: a compact set lies in such a ball.

def HCPolySupport.HighContrast.regCoeffFieldOfBallPointwiseElliptic {d : ℕ} (f : CoeffField d) (hfm : Measurable f) (hfp : ∀ (R : ℝ), 0 < R → ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ x ∈ Metric.ball 0 R, IsEllipticMatrix lam Lam (f x)) : RegCoeffField d

A measurable field uniformly elliptic at every point of every ball around the origin, with that ball's own constants, is a regular coefficient field: its entries are bounded on each ball by the upper ellipticity constant there, hence locally integrable.

Equations

• HCPolySupport.HighContrast.regCoeffFieldOfBallPointwiseElliptic f hfm hfp = { toFun := f, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.regCoeffFieldOfBallPointwiseElliptic_toFun {d : ℕ} (f : CoeffField d) (hfm : Measurable f) (hfp : ∀ (R : ℝ), 0 < R → ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ x ∈ Metric.ball 0 R, IsEllipticMatrix lam Lam (f x)) : (regCoeffFieldOfBallPointwiseElliptic f hfm hfp).toFun = f

theorem HCPolySupport.HighContrast.aeLocallyUniformlyEllipticField_of_ball_pointwise {d : ℕ} {f : CoeffField d} (hfm : Measurable f) (hfp : ∀ (R : ℝ), 0 < R → ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ x ∈ Metric.ball 0 R, IsEllipticMatrix lam Lam (f x)) : Book.Ch04.AELocallyUniformlyEllipticField (regCoeffFieldOfBallPointwiseElliptic f hfm hfp)

Pointwise uniform ellipticity on every ball gives locally uniform almost everywhere ellipticity: a triadic cube lies in a ball, whose constants serve it.

theorem HCPolySupport.HighContrast.blockPosDef_coarseBlock {d : ℕ} [NeZero d] (m : ℤ) (a : CoeffSpace d) : Book.Ch02.BlockPosDef (coarseBlock (centeredCube d m) a)

The coarse response of a sample is positive definite on every centered triadic cube.

theorem HCPolySupport.HighContrast.blockPosDef_annealedBlock_centeredCube {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (m : ℤ) (hint : HasIntegrableCoarseBlock P (centeredCube d m)) : Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d m))

The annealed block is positive definite once the coarse response is integrable over the law.