Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.UnitCubeDirichletDivergenceResponse

High-contrast homogenization: Provider.Regularity.UnitCubeDirichletDivergenceResponse #

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

A selected identity Dirichlet response on the unit cube #

Every proof-carrying Euclidean L² vector field on the centered unit cube defines an admissible datum for the identity Dirichlet divergence problem. This module selects one weak zero-trace response and records its defining weak equation. No pointwise uniqueness of H10Function representatives is asserted.

source
theorem HCPolySupport.HighContrast.unitCubeEuclideanL2Field_memLp_normalizedCubeMeasure {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
MeasureTheory.MemLp F.toField 2 (normalizedCubeMeasure (originCube d 0))

A proof-carrying unit-cube Euclidean L² field is an ambient vector L² datum for the normalized cube measure.

source
theorem HCPolySupport.HighContrast.exists_unitCubeDirichletDivergenceResponse {d : ℕ} [NeZero d] (F : UnitCubeEuclideanL2Field d) :
∃ (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w F.toField

Every proof-carrying Euclidean L² datum on the centered unit cube has an identity-coefficient zero-trace weak response.

source
noncomputable def HCPolySupport.HighContrast.unitCubeDirichletDivergenceResponse {d : ℕ} [NeZero d] (F : UnitCubeEuclideanL2Field d) :
H10Function (openCubeSet (originCube d 0))

A selected identity-coefficient zero-trace weak response to a unit-cube Euclidean L² datum. The selection is characterized below only by the weak equation, which is the representative-invariant property used downstream.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.unitCubeDirichletDivergenceResponse_problem {d : ℕ} [NeZero d] (F : UnitCubeEuclideanL2Field d) :
    CubeDirichletDivergenceProblem (originCube d 0) (unitCubeDirichletDivergenceResponse F) F.toField

    The selected response satisfies the identity Dirichlet divergence problem with exactly the supplied datum.