Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationGeometric

High-contrast homogenization: #

Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationGeometric

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

Geometric continuous K control of the rounded affine iteration #

The rounded affine response is iterated from zero. Consecutive response differences obey the strict contraction selected before the matrix and forcing. The first increment is treated separately by the identity Dirichlet estimate, so its finiteness is derived from the forcing energy and is never assumed for an output gradient.

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

The zero-started rounded affine response iteration.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIteration_zero {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) :
    roundedUnitCubeDirichletContinuousKIteration abar hS h 0 = 0
    source
    @[simp]
    theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIteration_succ {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) :
    roundedUnitCubeDirichletContinuousKIteration abar hS h (n + 1) = roundedUnitCubeDirichletContinuousKIterationStep abar hS h (unitCubeGradientEuclideanL2Field (roundedUnitCubeDirichletContinuousKIteration abar hS h n))
    source
    noncomputable def HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrement {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) :
    UnitCubeEuclideanL2Field d

    The gradient-field increment between two consecutive affine responses.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.unitCubeGradientEuclideanL2Field_sub {d : ℕ} (u v : H10Function (openCubeSet (originCube d 0))) :
      unitCubeGradientEuclideanL2Field (u - v) = unitCubeEuclideanL2FieldSub (unitCubeGradientEuclideanL2Field u) (unitCubeGradientEuclideanL2Field v)

      Packaging a difference after taking the gradient agrees with pointwise subtraction of the two packaged gradients.

      source
      theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIteration_succ_problem {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) :
      CubeDirichletDivergenceProblem (originCube d 0) (roundedUnitCubeDirichletContinuousKIteration abar hS h (n + 1)) (unitCubeEuclideanL2FieldAdd h (unitCubeEuclideanL2FieldConstMatrixMul (roundedReferenceMatrix abar hS - 1) (unitCubeGradientEuclideanL2Field (roundedUnitCubeDirichletContinuousKIteration abar hS h n)))).toField

      Every successor iterate satisfies the literal affine identity Dirichlet problem generated by the preceding gradient.

      source
      theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIteration_one_problem {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) :
      CubeDirichletDivergenceProblem (originCube d 0) (roundedUnitCubeDirichletContinuousKIteration abar hS h 1) h.toField

      The first iterate solves the identity problem with exactly the original forcing; the defect term vanishes because the iteration starts at zero.

      source
      theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrement_zero {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) :
      roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h 0 = unitCubeGradientEuclideanL2Field (roundedUnitCubeDirichletContinuousKIteration abar hS h 1)

      The zeroth packaged increment is exactly the packaged gradient of the first response.

      source
      theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletContinuousKIterationIncrementGeometricBound (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) < ⊤

      For each positive dimension, the fractional order, strict contraction, and initial-response constant are fixed before all matrix and forcing data. Finite forcing energy gives a finite first increment, and every later increment is bounded by the corresponding geometric power.