High-contrast homogenization:

Provider.Regularity.RoundedUnitCubeDirichletContinuousKDefectResponseDifferenceContraction

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

Difference contraction for the rounded affine response step

The selected identity response is specialized both to the rounded-reference identity defect and to the affine datum used by the perturbative iteration. Subtracting two affine-step weak equations cancels their common forcing and turns the response difference into the identity Dirichlet response to the defect acting on the datum difference. The previously selected small fractional order therefore contracts successive response differences with the same strict coefficient.

noncomputable def HCPolySupport.HighContrast.unitCubeEuclideanL2FieldSub {d : ℕ} (F G : UnitCubeEuclideanL2Field d) : UnitCubeEuclideanL2Field d

Pointwise subtraction, packaged on the unit-cube Euclidean L² carrier.

Equations

• HCPolySupport.HighContrast.unitCubeEuclideanL2FieldSub F G = { toField := fun (x : HCPolySupport.Vec d) => F.toField x - G.toField x, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.unitCubeEuclideanL2FieldSub_apply {d : ℕ} (F G : UnitCubeEuclideanL2Field d) (x : Vec d) : (unitCubeEuclideanL2FieldSub F G).toField x = F.toField x - G.toField x

noncomputable def HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationStep {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h F : UnitCubeEuclideanL2Field d) : H10Function (openCubeSet (originCube d 0))

One affine Picard step: solve the identity Dirichlet problem with the common forcing plus the rounded-reference defect acting on the current gradient field.

Equations

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

theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationStep_problem {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h F : UnitCubeEuclideanL2Field d) : CubeDirichletDivergenceProblem (originCube d 0) (roundedUnitCubeDirichletContinuousKIterationStep abar hS h F) (unitCubeEuclideanL2FieldAdd h (unitCubeEuclideanL2FieldConstMatrixMul (roundedReferenceMatrix abar hS - 1) F)).toField

The selected affine step satisfies its defining identity Dirichlet weak equation with the forcing and rounded defect kept as a literal sum.

theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletContinuousKIterationStepDifferenceContraction (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ENNReal.ofReal A ^ (2 * ↑s) < ENNReal.ofReal (101 / 100) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < ENNReal.ofReal (101 / 1000000) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < 1 ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h F G : UnitCubeEuclideanL2Field d), unitCubeNormalizedContinuousKEnergy s (unitCubeGradientEuclideanL2Field (roundedUnitCubeDirichletContinuousKIterationStep abar hS h F - roundedUnitCubeDirichletContinuousKIterationStep abar hS h G)) ≤ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) * unitCubeNormalizedContinuousKEnergy s (unitCubeEuclideanL2FieldSub F G)

For each positive dimension, the small order and contraction coefficient selected before all analytic inputs contract the difference of any two selected rounded defect responses by the energy of the datum difference.