Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.PhysicalScaleTransport

High-contrast homogenization: Provider.Quenched.PhysicalScaleTransport #

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

Physical-scale coefficient transport #

Triadic restoration acts on the a.e.-quotient coefficient space by the pullback a ↦ (x ↦ a(3^N x)). It is measurable for the coefficient-space sigma-field, and a coarse block on a restored cell is exactly the original coarse block at the generation shifted by N.

source
theorem HCPolySupport.HighContrast.Quenched.quasiMeasurePreserving_triadicDilateVec {d : ℕ} (N : ℕ) :
MeasureTheory.QuasiMeasurePreserving (triadicDilateVec N) MeasureTheory.volume MeasureTheory.volume
source
theorem HCPolySupport.HighContrast.Quenched.isAELocallyUniformlyElliptic_rescaleCoeffField {d : ℕ} (N : ℕ) (a : CoeffSpace d) :
IsAELocallyUniformlyElliptic (rescaleCoeffField N ↑↑a)

The triadic dilation carries the ball of radius R into the ball of radius 3^N R, so a locally uniformly elliptic field stays one under rescaling.

source
theorem HCPolySupport.HighContrast.Quenched.triadicDilateVec_mem_openCubeSet {d : ℕ} (N : ℕ) (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet (Book.Ch02.dilateCube (-↑N) Q)) :
triadicDilateVec N x ∈ openCubeSet Q

The triadic dilation carries the open cube shrunk by N generations into the open cube.

source
noncomputable def HCPolySupport.HighContrast.Quenched.physicalScaleCoefficient {d : ℕ} (N : ℕ) (a : CoeffSpace d) :
CoeffSpace d

The coefficient restored at generation N, represented by x ↦ a(3^N x) on the a.e.-quotient coefficient space.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.physical_scale_coeff_ae {d : ℕ} (N : ℕ) (a : CoeffSpace d) :
    ↑↑(physicalScaleCoefficient N a) =ᵐ[MeasureTheory.volume] rescaleCoeffField N ↑↑a

    The quotient representative of the restored coefficient is the literal triadic rescaling of the original representative almost everywhere.

    source
    theorem HCPolySupport.HighContrast.Quenched.measurable_physical_scale_coeff {d : ℕ} (N : ℕ) :
    Measurable (physicalScaleCoefficient N)

    Triadic restoration is measurable on the a.e.-quotient coefficient space, so its pushforward law is well-defined.

    source
    noncomputable def HCPolySupport.HighContrast.Quenched.physicalScaleCoefficientOn {d : ℕ} (N : ℕ) (a : CoeffSpace d) (Q : TriadicCube d) :
    Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (Book.Ch02.dilateCube (-↑N) Q))

    The rescaled coefficient, read on the cube shrunk by N generations, with the ellipticity constants the sample carries on the original cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.coarseBlock_standardCell_physical_scale_coeff {d : ℕ} (N : ℕ) (m : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) :
      coarseBlock (standardCell d m w) (physicalScaleCoefficient N a) = coarseBlock (standardCell d (↑N + m) w) a

      Coarse blocks on a hatted scale are exactly coarse blocks of the original coefficient at the corresponding physical generation.

      source
      theorem HCPolySupport.HighContrast.Quenched.blockExcess_coarseBlock_standardCell_physical_scale_coeff {d : ℕ} (N : ℕ) (m : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (Abar : BlockMat d) :
      blockExcess (coarseBlock (standardCell d m w) (physicalScaleCoefficient N a)) Abar = blockExcess (coarseBlock (standardCell d (↑N + m) w) a) Abar

      The normalized positive excess is unchanged by the physical-scale coarse-block transport.