Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.CellFamilyAndFluxRow

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.CellFamilyAndFluxRow

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

Cell-based physical forced families and the flux-response row #

This module constructs a zero-forcing cube solution by restricting the physical weak solution to each cell of an enlarged-margin ruled Whitney system. It then prices the resulting physical flux-defect row by the coarse flux-response row.

Almost-everywhere invariance #

source
theorem HCPolySupport.HighContrast.RowSupply.cubeBesovDualFullNorm_congr_ae_on_ruledCell {d : ℕ} (Q : TriadicCube d) (s : ℝ) {f g : Vec d → ℝ} (hfg : f =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] g) :
cubeBesovDualFullNorm Q s 2 2 f = cubeBesovDualFullNorm Q s 2 2 g
source
theorem HCPolySupport.HighContrast.RowSupply.physicalFullDualBesovVectorNorm_congr_ae_on_ruledCell {d : ℕ} (Q : TriadicCube d) (s : ℝ) {F G : Vec d → Vec d} (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) :
physicalFullDualBesovVectorNorm Q s F = physicalFullDualBesovVectorNorm Q s G
source
theorem HCPolySupport.HighContrast.RowSupply.physicalFullDualWhitneyFamilyCellEnergy_congr_ae_on_ruledCell {d : ℕ} {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (F G : system.CellIndex → Vec d → Vec d) (hFG : ∀ (i : system.CellIndex), F i =ᵐ[MeasureTheory.volume.restrict (system.cell i)] G i) (i : system.CellIndex) :
physicalFullDualWhitneyFamilyCellEnergy system s F i = physicalFullDualWhitneyFamilyCellEnergy system s G i

The full-dual Whitney cell energy is invariant under almost-everywhere equality on an enlarged-margin ruled cell.

The forced equation on one cell #

source
theorem HCPolySupport.HighContrast.RowSupply.exists_cellCoeffFamily_and_forcedEquation {d : ℕ} {U : Set (Vec d)} (aSource : Source.AKL.Field d) (haSource : AEUniformlyEllipticField aSource) (aPhysical : CoeffField d) (haeSource : ↑aSource =ᵐ[MeasureTheory.volume] aPhysical) (u : H1Function U) (huPhysical : IsWeakSolutionOn aPhysical U u.grad) (Q : TriadicCube d) (hQ : openCubeSet Q ⊆ U) :
∃ (aCell : Book.Ch03.CoeffFamily d) (uCell : H1Function (openCubeSet Q)), (aCell.coeffOn Q).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet Q)] aPhysical ∧ (∀ (x : Vec d), uCell.grad x = u.grad x) ∧ Book.Ch03.IsForcedEquation Q aCell uCell 0

A physical weak solution restricts to a zero-forcing solution on every triadic cube contained in its domain.

The family over the enlarged-margin ruled system #

source
def HCPolySupport.HighContrast.RowSupply.RuledCellPhysicalForcedFamily {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (aPhysical : CoeffField d) (u : H1Function U) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) :
Prop

On each ruled cell, the coefficient family agrees almost everywhere with the physical coefficient and the forced solution has the physical gradient.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.RowSupply.exists_ruledCellPhysicalForcedFamily {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (aSource : Source.AKL.Field d) (haSource : AEUniformlyEllipticField aSource) (aPhysical : CoeffField d) (haeSource : ↑aSource =ᵐ[MeasureTheory.volume] aPhysical) (u : H1Function U) (huPhysical : IsWeakSolutionOn aPhysical U u.grad) :
    ∃ (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0), RuledCellPhysicalForcedFamily system aPhysical u aCell wCell

    The cell-based physical forced family exists over every enlarged-margin ruled Whitney system.

    The flux-response row #

    source
    noncomputable def HCPolySupport.HighContrast.RowSupply.coarseFluxResponseConstant (d : ℕ) :
    ℝ

    The explicit constant in the coarse flux-response estimate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.RowSupply.physicalFluxDefectRow_le_coarseResponseRow {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hs : 0 < s) (hsOne : s < 1) (aPhysical : CoeffField d) (u : H1Function U) (a0 : system.CellIndex → Book.Ch03.ConstantCoeffMatrix d) (aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aPhysical u aCell wCell) :
      normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system s (ruledPhysicalFluxDefectOnCell system aPhysical a0 u)) ≤ normalizedWhitneyRowEnergy system fun (i : system.CellIndex) => ENNReal.ofReal (physicalDualBesovScaleFactor (whitneyCellCube system i) s * Book.Ch03.coarseFluxResponseWithRHSRHS (coarseFluxResponseConstant d) (whitneyCellCube system i) (aCell i) (a0 i) s 0 (wCell i)) ^ 2

      The physical flux-defect row is bounded by the coarse flux-response row of the cell-based forced family.