High-contrast homogenization:

Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationWeakLimit

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

Zero-trace weak limit of the rounded affine iteration

The geometric continuous-K increment estimates are kept together with the base Hilbert L² convergence. Closedness of the zero-trace gradient range recovers an honest H10Function at the limit. The affine identity equations then pass to the limit against each fixed zero-trace test gradient and give the rounded constant-coefficient weak equation.

theorem HCPolySupport.HighContrast.unitCubeGradientEuclideanL2FieldHilbertL2_eq_gradToHilbertVectorL2 {d : ℕ} (u : H10Function (openCubeSet (originCube d 0))) : unitCubeEuclideanL2FieldHilbertL2 (unitCubeGradientEuclideanL2Field u) = u.gradToHilbertVectorL2

The Hilbert representative of a packaged unit-cube gradient is the standard Hilbert L² realization of that weak gradient.

noncomputable def HCPolySupport.HighContrast.unitCubeMatrixGradientTestHilbertL2 {d : ℕ} (A : Mat d) (φ : H10Function (openCubeSet (originCube d 0))) : ↥(HilbertVectorL2 (openCubeSet (originCube d 0)))

A matrix-transposed test gradient, packaged in the Hilbert L² space so that pairing it with a solution gradient represents the coefficient weak form.

Equations

• HCPolySupport.HighContrast.unitCubeMatrixGradientTestHilbertL2 A φ = HCPolySupport.toHilbertVectorL2OfVecField ⋯

theorem HCPolySupport.HighContrast.inner_unitCubeMatrixGradientTestHilbertL2_eq_integral {d : ℕ} (A : Mat d) (φ u : H10Function (openCubeSet (originCube d 0))) : inner ℝ (unitCubeMatrixGradientTestHilbertL2 A φ) u.gradToHilbertVectorL2 = ∫ (x : Vec d) in openCubeSet (originCube d 0), vecDot (matVecMul A (u.grad x)) (φ.grad x)

Pairing with the transposed matrix test gradient is exactly the weak constant-coefficient bilinear form.

theorem HCPolySupport.HighContrast.exists_h10Function_of_tendsto_roundedIterationGradientHilbertL2 {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (G : ↥(HilbertVectorL2 (openCubeSet (originCube d 0)))) (hG : Filter.Tendsto (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h) Filter.atTop (nhds G)) : ∃ (u : H10Function (openCubeSet (originCube d 0))), u.gradToHilbertVectorL2 = G

A Hilbert L² limit of honest zero-trace gradients is again the gradient of an honest zero-trace function on the open unit cube.

theorem HCPolySupport.HighContrast.roundedIteration_isZeroTraceDirichletRhsWeakSolution_of_tendsto {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (u : H10Function (openCubeSet (originCube d 0))) (hlim : Filter.Tendsto (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h) Filter.atTop (nhds u.gradToHilbertVectorL2)) : IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d 0)) u fun (x : Vec d) => -h.toField x

Passing the affine identity problems to an identified zero-trace gradient limit gives the rounded constant-coefficient Dirichlet equation.

theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletContinuousKIterationWeakLimit (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 ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d), unitCubeNormalizedContinuousKEnergy s h < ⊤ → unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h 0) ≤ ENNReal.ofReal B ^ (2 * ↑s) * unitCubeNormalizedContinuousKEnergy s h ∧ unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h 0) < ⊤ ∧ (∀ (n : ℕ), unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h n) ≤ (ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2)) ^ n * unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h 0) ∧ unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h n) < ⊤) ∧ ∃ (u : H10Function (openCubeSet (originCube d 0))), Filter.Tendsto (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h) Filter.atTop (nhds u.gradToHilbertVectorL2) ∧ IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d 0)) u fun (x : Vec d) => -h.toField x

The dimension-first order, geometric increment bounds, and their zero-trace rounded-reference weak limit are selected in one package. This keeps the exact same witnesses available to the subsequent positive-order closure argument.