Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationL2Limit

High-contrast homogenization: #

Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationL2Limit

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

Base L2 limit of the rounded affine iteration #

The gradient iterates are embedded in the Hilbert-valued L² space on the open centered unit cube. On this unit cube, restricted volume is exactly the normalized cube measure. The geometric continuous-K increment bound controls the Hilbert L² distance, so completeness supplies an actual limit without cancelling any potentially infinite extended-real term.

source
theorem HCPolySupport.HighContrast.unitCubeEuclideanL2Field_memVectorL2 {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
MemVectorL2 (openCubeSet (originCube d 0)) F.toField

A proof-carrying normalized unit-cube field is a physical vector L² field on the open unit cube because that cube has volume one.

source
noncomputable def HCPolySupport.HighContrast.unitCubeEuclideanL2FieldHilbertL2 {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
↥(HilbertVectorL2 (openCubeSet (originCube d 0)))

The Hilbert-valued physical L² representative of a proof-carrying normalized unit-cube Euclidean field.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.norm_unitCubeEuclideanL2FieldHilbertL2 {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
    ‖unitCubeEuclideanL2FieldHilbertL2 F‖ = ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField).toReal

    The norm of the Hilbert representative is the real value of the normalized Euclidean extended L² norm.

    source
    theorem HCPolySupport.HighContrast.unitCubeEuclideanL2FieldHilbertL2_sub {d : ℕ} (F G : UnitCubeEuclideanL2Field d) :
    unitCubeEuclideanL2FieldHilbertL2 (unitCubeEuclideanL2FieldSub F G) = unitCubeEuclideanL2FieldHilbertL2 F - unitCubeEuclideanL2FieldHilbertL2 G

    The Hilbert representative respects pointwise subtraction.

    source
    theorem HCPolySupport.HighContrast.dist_unitCubeEuclideanL2FieldHilbertL2 {d : ℕ} (F G : UnitCubeEuclideanL2Field d) :
    dist (unitCubeEuclideanL2FieldHilbertL2 F) (unitCubeEuclideanL2FieldHilbertL2 G) = ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeEuclideanL2FieldSub F G).toField).toReal

    Hilbert L² distance is the real normalized Euclidean L² norm of the pointwise field difference.

    source
    theorem HCPolySupport.HighContrast.unitCubeNormalizedEuclideanLpENorm_sq_le_continuousKEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
    (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 ≤ unitCubeNormalizedContinuousKEnergy s F

    The normalized Euclidean L² square is the first, nonnegative term of the quadratic continuous-K energy.

    source
    noncomputable def HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) :
    ↥(HilbertVectorL2 (openCubeSet (originCube d 0)))

    The Hilbert L² sequence formed by the packaged gradients of the zero-started rounded affine responses.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.dist_roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2_succ {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) :
      dist (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h n) (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h (n + 1)) = ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h n).toField).toReal

      Consecutive Hilbert L² distance is exactly the real normalized Euclidean L² size of the corresponding packaged gradient increment.